Why is this Symbolic Execution with Z3 resulting in an error?

Question

I am trying to generate test cases using a symbolic execution logic based on the SMT Solver Z3.

I have the following code.

void foo(int a, int b, int c){
    int x = 0, y = 0, z = 0;
    if(a){
        x = -2;
    }

    if (b < 5){
        if (!a && c) { y = 1; }
        z = 2;
    }

    assert(x + y + z != 3);
}

Now, an error occurs during the SMT Solving process and the resulting error log is like below.

(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-option :produce-proofs true)
(define-sort bot () Int)

(declare-const sv_1 Int)
(declare-const sv_5 Int)
(define-fun strcmp ((a String) (b String)) Int (ite (= a b) 0 1))

(assert (! (not (= sv_1 0)) :named __a0))
(assert (! (< sv_5 5) :named __a1))
(assert (! (not (not (= sv_1 0))) :named __a2))
(assert (! (not (not (= (+ (+ (bvneg 2) 0) 2) 3))) :named __a3))
(check-sat)
(get-unsat-core)
(get-model)

I have done some testing with this code.

If I do not use x, y, z in the assert function, there is no error.

If the first 'if statement' is true (i.e. a != 0), then the program will never enter the 'if (!a && c) statement. If I erase one of these 'if statements', the there is no error. But I do not understand why this error is occurring. Could anyone explain to me why Z3 is not being able to solve this? Thank you.

Answer 1

You didn't tell us what exact error you're getting, so I'm assuming it comes from z3 and not from some other part of your toolchain. Let's run the SMTLib program you posted through z3. When I do that, z3 tells me that there's a "sort mismatch:"

(error "line 13 column 38: operator is applied to arguments of the wrong sort")

And this is because you've the line:

(assert (! (not (not (= (+ (+ (bvneg 2) 0) 2) 3))) :named __a3))

and in particular the expression (bvneg 2). The function bvneg is bit-vector negation, but 2 is an Integer, not a bit-vector value. You want to use regular negation instead. So, change that line to:

(assert (! (not (not (= (+ (+ (- 0 2) 0) 2) 3))) :named __a3))

With that change, z3 says:

unsat
(__a3)
(error "line 16 column 10: model is not available")

Great; so now you have unsat, and the unsat-core is __a3. The error in the last line can be ignored, it arises because you called get-model but the problem is unsatisfiable, and thus there is no model to display.

Now, you might wonder why this is unsat, perhaps you expected it to be satisfiable? You haven't told us how you converted your C function to SMTLib, and it appears that you used some unnamed tool to do so, perhaps one of your own creation. The tool clearly has a bug in it, as it created the bvneg expression that we fixed above, maybe it's not to be trusted as much! But let's see why z3 thinks this problem is unsat.

It boils down to these two lines that your tool generated:

(assert (! (not (= sv_1 0)) :named __a0))
(assert (! (not (not (= sv_1 0))) :named __a2))

Let's simplify these by dropping the annotations, and for clarity I'll rename sv_1 to a, since that seems to be the origin of the variable. This gives us:

(assert (not (= a 0)))
(assert (not (not (= a 0))))

Let's simplify a bit:

(assert (distinct a 0))
(assert (not (distinct a 0)))

(In SMTLib, (distinct x y) means (not (= x y)).)

And now we see the problem; you have two assertions the first one says a is not 0, and the second says it's not the case that a is not 0. Clearly, these two assertions conflict each other, and this is why z3 tells you unsat.

There's actually another source of conflict as well. The other assertion simplifies to:

(assert (not (not (= (+ (+ (- 0 2) 0) 2) 3)

which, if you do the arithmetic, says:

(assert (= 0 3))

which is clearly not true. (And this is why z3 tells you your unsat core is __a3; which is the root-cause of why the whole set of assumptions is unsatisfiable. Note that unsat-cores are not unique, and z3 does not guarantee it'll give you a minimal set. So it could've told you (__a0 __a2) as well as the unsat-core; but that's a separate discussion.)

So, z3 is doing the right thing given your generated SMTLib (after the correction mentioned above.)

Why your tool generates this SMTLib for the C-program is something we cannot help you with unless you tell us more about how you generated that output, or what this intermediate tool actually does. My rough guess is that it's actually generating a bunch of test cases, and eventually it comes to a point where it says "I don't have any more test cases to generate" so everything is actually fine; but there seems to be some issue with why it would generate the (get-model) call; or why it would do the bvneg call which is incorrect. But otherwise, you'll have to consult with the developers of the tool that generates this SMTLib for you for further debugging.