Z3 going from unknown to unsat when changing names of constants

[clairedross]

Hello z3 team,

I have found a strange case where a VC status changes from unknwon to unsat when renaming some constants. The two attached VCs are identical, except for the names of two constants, i4 and j4 in assert_4 and i5 and j5 in assert_5. However, z3 returns unsat immediately on assert_4 and unknown immediately on assert_5. I understand that z3 is not complete when quantifiers are involved, and that names of constants can influence its behavior (if for example constants are hashed). What surprises me is the transition from unsat to unknown as unknown means that the prover does not have anything to do anymore, right?

Thanks for your help, -- Claire Dross, PhD Software Engineer dross@adacore.com

assert_4_smt2.txt assert_5_smt2.txt

[wintersteiger]

Thanks for the example, we'll take a closer look at this. In general though, "unknown" means that the solver gave up (for whatever reason). It doesn't mean there's nothing else to do, it just means it didn't know what else to try.

[NikolajBjorner]

Note, the return unsat/unknown also fluctuates if you vary the random seed:

Example:

        z3 assert_4.smt2 smt.random_seed=4
       unknown

       z3 assert_4.smt2 smt.random_seed=5
       unsat

[clairedross]

On 08/03/2017 10:25, Nikolaj Bjorner wrote:

Note, the return unsat/unknown also fluctuates if you vary the random seed:

Example:

|z3 assert_4.smt2 smt.random_seed=4 unknown z3 assert_4.smt2 smt.random_seed=5 unsat |

Interesting, so z3 has indeed some random behavior that influences whether it finds something to try on a VC. I would have thought random seeds only influenced the way z3 was going through the search space.

Thanks for this insight,

-- Claire

[NikolajBjorner]

well, we still need to explain what is going on.

[NikolajBjorner]

The benchmark uses the theory of arrays, and ends up instantiating arrays using auxiliary functions that are defined in the model. These auxiliary functions are not defined with the instantiation, so the solver may be unable to use them in finding unsat.

For example, a model may define the function k!79, which is used in an (_ as-array k!79) expression.

(define (k!79 x!0) (if (= x!0 5) (mkrep (mksplit_fields natural!val!2 natural!val!0 natural!val!1)) (if (= x!0 (- 8851)) (mkrep (mksplit_fields natural!val!2 natural!val!2 natural!val!7)) (mkrep (mksplit_fields natural!val!2 natural!val!0 natural!val!1)))))

By the time these instantiations are used, there is no information what k!80 and k!79 are.

In the end, the theory of arrays decides that it cannot for sure say whether the formula is sat because there is no complete support for as-array.

I don’t see a simplistic fix here as Z3 does not have lambdas at this point. Lambdas could be very nice for several reasons, but also a somewhat substantial change. In lieu of lambdas we could expose what these functions k!80 etc. are when the instantiations are used. It amounts to asserting the macro axiom for these functions when the instantiations are invoked. This could introduce regressions. While MBQI wasn't designed with the theory of arrays in mind, it rather assumes that arrays are encoded directly using quantified formulas, we would of course like to get the integration of the various features to play along.