SMT backend encounters 'Queue.nth: internal error'

[will62794]

I encountered a Queue.nth: internal error message when trying to prove a simple TLAPS theorem using an SMT backend. I first noticed this in the Toolbox, but also reproduced it from the command line. If I run

tlapm --cleanfp --toolbox 183 184 consensus_wo_decide.tla

in the directory of the attached zip file, I see the following error in the tlapm output:

@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:184:65:184:67
@!!status:failed
@!!prover:smt
@!!meth:time-limit: 5
@!!reason:Queue.nth: internal error
@!!already:false
@!!obl:
ASSUME NEW CONSTANT Node,
       NEW VARIABLE vote_request_msg,
       NEW VARIABLE voted,
       NEW VARIABLE vote_msg,
       NEW VARIABLE votes,
       NEW VARIABLE leader,
       NEW VARIABLE voting_quorum
PROVE  (\A i, j, k \in Node : voted[j] \/ (~<<j, i>> \in vote_msg /\ TRUE))
       /\ (\E i, j \in Node :
              /\ ~voted[i]
              /\ <<j, i>> \in vote_request_msg
              /\ vote_msg' = vote_msg \cup {<<i, j>>}
              /\ voted' = [voted EXCEPT ![i] = TRUE]
              /\ UNCHANGED <<vote_request_msg, votes, leader, voting_quorum>>)
       => (\A i, j, k \in Node : voted[j] \/ (~<<j, i>> \in vote_msg /\ TRUE))'

@!!END

This seems to indicate some kind of error that occurs even before the SMT query is sent to the solver i.e. Queue.nth appears to be an OCaml based error.

[will62794]

Also, I am using the following version of tlapm:

1.4.5 (build 33809)

on an M1 Macbook Air, macOS 11.4.

[will62794]

@johnyf Any initial thoughts on what might be causing this error?

[muenchnerkindl]

Unfortunately, it's a problem that we see frequently. My usual workaround is to decompose the proof obligation. It would be great if Ioannis was able to track down the root cause.

[johnyf]

Thank you for reporting this error. Before the function

https://github.com/tlaplus/tlapm/blob/b82e2fd049c5bc1b14508ae16890666c6928975f/src/backend/smt.ml#L492

is called, all De Bruijn indices are positive. Within the function process_obligation, an expression Ix -1 arises, and raises an exception when the following line is reached:

https://github.com/tlaplus/tlapm/blob/b82e2fd049c5bc1b14508ae16890666c6928975f/src/backend/smt.ml#L514

The exception is raised at:

https://github.com/tlaplus/tlapm/blob/b82e2fd049c5bc1b14508ae16890666c6928975f/src/typesystem/typ_t.ml#L655

The next thing to locate is where the -1 index is created.