Unpredictable Timeouts when Array Value Bounds

[dz333]

We are using the most recent release of z3 (4.12.1).

We frequently work with arrays whose values are bounded (e.g., between 0 and 7).

Placing these bounds constraints tends to decrease the predictability of Z3's ability to find models for simple constraints.

We have a lot of complicated examples where removing the bounds constraints leads to finding models instantly where otherwise Z3 hangs.

Here is a trivial example where we just assert that two arrays have the same values at a few indices:

(declare-fun t () (Array Int Int))
(assert (forall ((x Int)) (<= 0 (select t x))))  ;; value bounds
(assert (forall ((x Int)) (<= (select t x) 1)))  ;; value bounds

(declare-fun tn () (Array Int Int))
(assert (forall ((x Int)) (<= 0 (select tn x)))) ;; value bounds
(assert (forall ((x Int)) (<= (select tn x) 1))) ;; value bounds

(assert (= (select tn 0) (select t 0))) ;; 
(assert (= (select tn 1) (select t 1))) ;; removing  this allows SAT to be found (but removing the one above does not)
(check-sat)                                                                                                                                                                            

If we remove some (or all) of the value bounds constraints z3 can find a model, or if we ONLY check the index 0 of both arrays, z3 can find a model.

---

Interestingly, if we change the bounds to 0 <= array[i] <= 2, then z3 will find a model for the above constraints:

(declare-fun t () (Array Int Int))
(assert (forall ((x Int)) (<= 0 (select t x))))  ;; value bounds
(assert (forall ((x Int)) (<= (select t x) 2)))  ;; value bounds

(declare-fun tn () (Array Int Int))
(assert (forall ((x Int)) (<= 0 (select tn x)))) ;; value bounds
(assert (forall ((x Int)) (<= (select tn x) 2))) ;; value bounds

(assert (= (select tn 0) (select t 0)))
(assert (= (select tn 1) (select t 1)))
(check-sat)                                                                                                                                                                            

So it seems like these value bounds are perhaps influencing Z3's reasoning about indices.

[NikolajBjorner]

Model-based quantifier instantiation in the main solver is not well suited for the theory of arrays. It relies on point-fixes to deal with array models. It means that model finding for quantified formulas works poorly with arrays. The main way ahead is to use a different core: using sat.smt=true enables an entirely different core which appears to fare better.

[dz333]

Excellent, thanks for the tip -- this seems to be a working first next step