3

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

Thomas
  • 31
  • 1
  • 1
    If you're going to work with C-like integers and unless this is an exercise in manual encoding, I suggest you use bitvectors rather than mathematical integers. – Philippe Jan 25 '12 at 21:20
  • 3
    Quick comment: this incorrect result is due to a bug in the Z3 formula preprocessor. It has been fixed, and the fix will be available in the next release. The bug affects benchmarks that use formulas of the form : `(mod (+ a b))` or `(mod (* a b))`. – Leonardo de Moura Jan 29 '12 at 03:04
  • @GManNickG: Good point, I will do it. – Leonardo de Moura Feb 02 '13 at 13:32

1 Answers1

2

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.

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53