CODEWITHSUNDEEP
z3
jchen
jchen

Reputation: 19

Z3 variable name causing "unknown" satisfiability

Using Z3 to check the satisfiability of

(declare-fun length ((Array Int Int)) Int)

(declare-const lindx2 (Array Int Int))
(declare-const findx1 (Array Int Int))
(declare-const orig_findx1 (Array Int Int))

(assert (and
  (forall ((i Int) (j Int))
    (let ((a!1 (and (<= 0 i)
                    (<= i (- (length findx1) 1))
                    (<= 0 j)
                    (<= j (- (length orig_findx1) 1))
                    (= i j))))
      (=> a!1 (= (select findx1 i) (select orig_findx1 j)))))
  (= (length lindx2) 11)
  (forall ((i Int)) (=> (and (<= 3 i) (<= i 25)) (= (select findx1 i) (- 1))))))
(check-sat)

returns unknown. This essentially tries to assert that all elements in findx1 and orig_findx1 are equal, that length(lindx2)=11, and that findx1[i]=-1 for i=[3,25]. However, changing "findx1" to "indx1" allows Z3 to return satisfiable. Does anyone know what might be causing the unknown satisfiability? I am using Z3 version 4.8.8 on Ubuntu 18.04

Upvotes: 0

Views: 130

Answers (2)

alias
alias

Reputation: 30475

I can replicate this, and it is really bizarre!

I'm not surprised this benchmark is unknown since it's full of quantifiers and it'd be hard to solve for z3. But changing findx1 to indx1 should have no impact on this; i.e., it should remain unknown.

I've reported this at https://github.com/Z3Prover/z3/issues/4600. The response is: It is MBQI that ends up failing to determine satisfiability. It is tied to array models. MBQI is more stable when you replace arrays by uninterpreted functions. That is, these sorts of discrepancies are unfortunately par for the course. Too bad!

Upvotes: 0

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

This is unfortunately (albeit for technical reasons) not surprising: it has been observed many times before that syntactic changes (renaming symbols, reordering SMT commands) cause performance and unknown/sat fluctuations, see e.g. https://github.com/Z3Prover/z3/issues/909/. It seems that Z3's heuristics are affected by the program structure, even when explicitly setting random seeds.

Upvotes: 0

Related Questions