(error "query failed: Sorts (Array Int Int) and Int are incompatible") on instance that should likely be SAT

[markusscherer]

When trying to solve an smtlib-instance we generated from a higher level representation, we encountered the error:

(error "query failed: Sorts (Array Int Int) and Int are incompatible")
unknown

We reproduced the error in versions 4.8.3 and 4.8.4 and 4.8.5 (partially in Linux, partially on MacOS), 4.6.0 reports sat, current master (df405536) reports unsat.

Unfortunately we did not succeed in in generating a "minimal" example, as the smallest instance showing this behavior we found still had 35k lines. What we have is a minimally different set of files, where adding two rules and a predicate changes a sat-instance to an instance exhibiting the error.

instances.zip

[NikolajBjorner]

@agurfinkel

While the crash doesn't reproduce in the latest master the bug that is exposed in previous versions remains.
The code that handles arrays expects stores whenever it is marked. https://github.com/Z3Prover/z3/blob/master/src/qe/qe_arrays.cpp#L392
However, in this case it doesn't have a store expression, but an "ite".
The test should be at least strengthened to include && m_arr_u.is_store(a_lhs)

A good idea is to make code like this:

  idxs.append(a_lhs->get_num_args() - 2, a_lhs->get_args() + 1);

validate that a_lhs is in fact an array by using a helper function. get_array_indices(a_lhs), get_num_array_indices(a_lhs) or similar.

[agurfinkel]

I will need some time to process this.
However, the requirement for that code is that the input is a conjunction of convex literals.
ite terms are neither expected nor supported. They should have been simplified using
model based implicant computation.

Maybe I am missing something...

[agurfinkel]

@NikolajBjorner digging deeper into this example, there is a problem with model evaluator. I get the following assertion failure:

-------- [qe] linearize ../src/qe/qe_arith.cpp:67 ---------
(= MState_0_4904!slice!5_4_n
   (store (store ((as const (Array Int Int)) 0) 64 96)
          96
          95346918756310292697882537094886449535797654316421409133056955209608488550400)) := (let ((a!1 (lambda ((x!1 Int))
             (ite (= x!1 64)
                  96
                  (ite (= x!1 96)
                       95346918756310292697882537094886449535797654316421409133056955209608488550400
                       0)))))
  (= a!1
     (store (store ((as const (Array Int Int)) 0) 64 96)
            96
            95346918756310292697882537094886449535797654316421409133056955209608488550400)))
------------------------------------------------

As you can see, the left hand side of the equality is evaluated as a lambda expression, the right as a store expression. The equality is not reduced to true, hence the assertion failure. However, more importantly, the mbp code is not prepared to deal with lambdas but might be getting them now because of the evaluator...

I'll keep digging further.

[agurfinkel]

changing model_evaluator.cpp:154 from

                //return m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE;

to

                return BR_DONE;

Restores the old behavior and makes the example pass (with sat). Not sure if it affects anything else though

[agurfinkel]

The previous behavior was to evaluate arrays as nested store-terms, unless model_compres=true. I would appreciate that this behavior remains, since it is used by seahorn. It seems that the only useful behavior is to evaluate arrays by lambda-terms when model_compress=false. This can be done as an extra option. The expansion of an array interpretation into a lambda term can be done at line 643 of model_evaluator.cpp. That is where currently arrays are expanded to store-terms by default.

[NikolajBjorner]

I believe the updates take care of Arie's issues with lambdas and crashes.
Would be good to double check end-to-end soundness of the solver.

[agurfinkel]

This does not address the root cause. For me, moves the assertion failure from one example to another. The solution makes QE code more robust, but the root cause is that array equalities are not evaluated correctly. PR with previously proposed solution submitted.

[NikolajBjorner]

@agurfinkel
The code here: https://github.com/Z3Prover/z3/blob/master/src/qe/qe_arrays.cpp#L246
It updates the m_has_stores_v when there is a term that has m_v as an argument and it is not select.
For example, if it is an "ite" term that as one of its arguments contains m_v, the term is marked.
Then in get_nesting_depth, marked terms that contain m_v are assumed to be a sequence of stores.

[NikolajBjorner]

is this addressed?