Wrong result from z3

Question

I'm trying to proof the following with Z3 SMT Solver: ((x*x) + x) = ((~x * ~x) + ~x). This is correct, because of overflow semantic in the c programming language.

Now I have written the following smt-lib code:

(declare-fun a () Int)

(define-fun myadd ((x Int) (y Int)) Int (mod (+ x y) 4294967296) )
(define-fun mynot ((x Int))         Int (- 4294967295 (mod x 4294967296)) )
(define-fun mymul ((x Int) (y Int)) Int (mod (* x y) 4294967296) )

(define-fun myfun1 ((x Int)) Int (myadd (mynot x) (mymul (mynot x) (mynot x))) )
(define-fun myfun2 ((x Int)) Int (myadd x (mymul x x)) )

(simplify (myfun1 0))
(simplify (myfun2 0))

(assert (= (myfun1 a) (myfun2 a)))
(check-sat)
(exit)

The output from z3 is:

0
0
unsat

Now my question: Why is the result "unsat"? The simplify command in my code shows that it is possible to get a valid allocation so that myfun1 and myfun2 have the same result.

Is something wrong with my code or is this a bug in z3?

Please can anybody help me. Thx

Answer 1

The incorrect result was due to a bug in the Z3 formula/expression preprocessor. The bug has been fixed, and is already part of the current release (v4.3.1). The bug affected benchmarks that use formulas of the form: (mod (+ a b)) or (mod (* a b)).

We can retry the example online here, and get the expected result.