Undefined solver evaluation leading to spurious counter-example

[rodrigo7491]

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 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).

Input specification

------ MODULE Oracle --------
EXTENDS Apalache, Integers

VARIABLES
  \* @type: Set(Set(Int));
  witness,
  \* @type: Bool;
  found

Init ==
  /\ witness \in {
    {{-1, 0, 5}, {0}},
    {{9}, {-2, -3}},
    {{1, 2}, {-1}}
    }
  /\ found \in BOOLEAN

Next ==
  UNCHANGED <<witness, found>>

NotFound ==
  ~found
======================

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:

---------------------------- 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.

(let ((a!1 (store (store (store ((as const (Array Int Bool)) false) (- 1) true)
                         0
                         true)
                  5
                  true)))
  (select (store (store ((as const (Array (Array Int Bool) Bool)) false)
                        a!1
                        true)
                 (store ((as const (Array Int Bool)) false) 0 true)
                 true)
          a!1))

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.