Potential correctness issue in integer arithmetic optimization

[merlinsun]

Hi,

I’ve encountered a potential correctness issue related to integer arithmetic optimization in Z3 https://github.com/Z3Prover/z3/commit/a51239c641b5fdcef66c5c477e7721946dae3188. 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!

[merlinsun]

I've just realized that this case involves non-linear arithmetic. If that makes the report out of scope, please feel free to close it.