Open
Description
Hi,
I’ve encountered a potential correctness issue related to integer arithmetic optimization in Z3 a51239c.
Specifically, Z3 appears to return an incorrect result for the objective function in the following example, while Optimathsat behaves as expected.
$ cat small.smt2
(declare-const a Int)
(declare-const b Int)
(assert (and (< 0 a) (>= a 1)))
(minimize (abs (div (div (- (div (- a) (- (abs (- (mod a 6)))))) b) b (abs (- b)))))
(check-sat)
(get-objectives)
$ z3 small.smt2
sat
(objectives
((let ((a!1 (- (abs (- (mod a 6))))))
(let ((a!2 (div (- (div (- a) a!1)) b)))
(abs (div (div a!2 b) (abs (- b)))))) (* (- 1) oo))
)
$ optimathsat small.smt2
sat
(objectives
((let ...) 0)
)Interestingly, if we slightly modify the expression — for example, replacing (abs (- b)) with (abs b) — Z3 produces the correct result:
$ cat pass.smt2
(declare-const a Int)
(declare-const b Int)
(assert (and (< 0 a) (>= a 1)))
(minimize (abs (div (div (- (div (- a) (- (abs (- (mod a 6)))))) b) b (abs b))))
(check-sat)
(get-objectives)
$ z3 pass.smt2
sat
(objectives
((let ((a!1 (- (abs (- (mod a 6))))))
(let ((a!2 (div (- (div (- a) a!1)) b)))
(abs (div (div a!2 b) (abs b))))) 0)
)I would appreciate it if you could take a look at this issue. Thank you!
Metadata
Metadata
Assignees
Labels
No labels