You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Z3's model evaluation might return UNDEF for some queries, which can make the decoder generate spurious counter-examples (among other problems), since Apalache currently equates UNDEF to false. So far this was only observed in nested set membership in the arrays encoding, see the spec below. This bug was found by Nitpicker (#1588).
Correct counter-example, currently the following is being generated:
---------------------------- MODULE counterexample ----------------------------
EXTENDS Oracle
(* Constant initialization state *)
ConstInit == TRUE
(* Initial state *)
State0 == found = TRUE /\ witness = {{0}}
(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation == found
================================================================================
Additional context
We are getting witness = {{0}} and not witness = {{-1, 0, 5}, {0}} because Z3's set membership check for {-1, 0, 5} via the model generated returns undefined, the checked expression is below.
Description
Z3's model evaluation might return
UNDEF
for some queries, which can make the decoder generate spurious counter-examples (among other problems), since Apalache currently equatesUNDEF
to false. So far this was only observed in nested set membership in the arrays encoding, see the spec below. This bug was found by Nitpicker (#1588).Input specification
The command line parameters used to run the tool
apalache-mc check --inv=NotFound --smt-encoding=arrays Oracle.tla
Expected behavior
Correct counter-example, currently the following is being generated:
Additional context
We are getting
witness = {{0}}
and notwitness = {{-1, 0, 5}, {0}}
because Z3's set membership check for{-1, 0, 5}
via the model generated returns undefined, the checked expression is below.Asserting this directly on Z3 gives a SAT result, so we should probably make a
check-sat
query for undefined results, instead of returning false.The text was updated successfully, but these errors were encountered: