Potential issue in arithmetic optimization #7677
Description
Hi,
I came across a potential correctness issue in the arithmetic optimization when using opt.optsmt_engine=symba. The two following inputs, which appear semantically similar, yield different objective values:
$ z3 opt.optsmt_engine=symba small_int.smt2
sat
(objectives
((- a) oo)
(a oo)
)
$ cat small_int.smt2
(set-option :opt.priority box)
(declare-const a Int)
(assert (< 0 (div a 0)))
(maximize (- a))
(maximize a)
(check-sat)
(get-objectives)
$ z3 opt.optsmt_engine=symba small_mix.smt2
sat
(objectives
((- a) 0)
(a 0)
)
$ cat small_mix.smt2
(set-option :opt.priority box)
(declare-const a Real)
(assert (< 0 (div (to_int a) 0)))
(maximize (- a))
(maximize a)
(check-sat)
(get-objectives)
Commit: 423930d