I ran into an interesting behaviour of Z3 when searching for all zeroes of polynomials within some interval. This is my problem statement:
(declare-fun perr () Real)
(assert
(let (($x10 (<= perr 1.0)))
(and (<= 0.0 perr) $x10)))
(assert
(let ((?x64 (^ perr 8.0)))
(let ((?x65 (* (- 9.0) ?x64)))
(let ((?x59 (^ perr 6.0)))
(let ((?x60 (* (- 4032.0) ?x59)))
(let ((?x55 (^ perr 5.0)))
(let ((?x56 (* 8064.0 ?x55)))
(let ((?x51 (^ perr 4.0)))
(let ((?x52 (* (- 10080.0) ?x51)))
(let ((?x46 (^ perr 3.0)))
(let ((?x47 (* 8064.0 ?x46)))
(let ((?x41 (^ perr 2.0)))
(let ((?x42 (* (- 4032.0) ?x41)))
(let ((?x69 (* 1152.0 perr)))
(let ((?x33 (^ perr 7.0)))
(let ((?x34 (* 1152.0 ?x33)))
(= (+ ?x34 ?x69 ?x42 ?x47 ?x52 ?x56 ?x60 ?x65) 144.0)))))))))))))))))
(check-sat)
(get-model)
This gives me the model
(
(define-fun perr () Real
(root-obj (+ (^ x 8) (* (- 128) (^ x 7)) (* 448 (^ x 6)) (* (- 896) (^ x 5)) (* 1120 (^ x 4)) (* (- 896) (^ x 3)) (* 448 (^ x 2)) (* (- 128) x) 16) 1))
)
I can ask Z3 for another model:
(declare-fun perr () Real)
(assert
(let (($x10 (<= perr 1.0)))
(and (<= 0.0 perr) $x10)))
(assert
(let ((?x64 (^ perr 8.0)))
(let ((?x65 (* (- 9.0) ?x64)))
(let ((?x59 (^ perr 6.0)))
(let ((?x60 (* (- 4032.0) ?x59)))
(let ((?x55 (^ perr 5.0)))
(let ((?x56 (* 8064.0 ?x55)))
(let ((?x51 (^ perr 4.0)))
(let ((?x52 (* (- 10080.0) ?x51)))
(let ((?x46 (^ perr 3.0)))
(let ((?x47 (* 8064.0 ?x46)))
(let ((?x41 (^ perr 2.0)))
(let ((?x42 (* (- 4032.0) ?x41)))
(let ((?x69 (* 1152.0 perr)))
(let ((?x33 (^ perr 7.0)))
(let ((?x34 (* 1152.0 ?x33)))
(= (+ ?x34 ?x69 ?x42 ?x47 ?x52 ?x56 ?x60 ?x65) 144.0)))))))))))))))))
(assert
(not (= perr (root-obj (+ (^ x 8) (* (- 128) (^ x 7)) (* 448 (^ x 6)) (* (- 896) (^ x 5)) (* 1120 (^ x 4)) (* (- 896) (^ x 3)) (* 448 (^ x 2)) (* (- 128) x) 16) 1))))
(check-sat)
This gives me
unsat
But if I do this incrementally, the solver cannot find unsat and times out:
(declare-fun perr () Real)
(assert
(let (($x10 (<= perr 1.0)))
(and (<= 0.0 perr) $x10)))
(assert
(let ((?x64 (^ perr 8.0)))
(let ((?x65 (* (- 9.0) ?x64)))
(let ((?x59 (^ perr 6.0)))
(let ((?x60 (* (- 4032.0) ?x59)))
(let ((?x55 (^ perr 5.0)))
(let ((?x56 (* 8064.0 ?x55)))
(let ((?x51 (^ perr 4.0)))
(let ((?x52 (* (- 10080.0) ?x51)))
(let ((?x46 (^ perr 3.0)))
(let ((?x47 (* 8064.0 ?x46)))
(let ((?x41 (^ perr 2.0)))
(let ((?x42 (* (- 4032.0) ?x41)))
(let ((?x69 (* 1152.0 perr)))
(let ((?x33 (^ perr 7.0)))
(let ((?x34 (* 1152.0 ?x33)))
(= (+ ?x34 ?x69 ?x42 ?x47 ?x52 ?x56 ?x60 ?x65) 144.0)))))))))))))))))
(check-sat)
(get-model)
(assert
(not (= perr (root-obj (+ (^ x 8) (* (- 128) (^ x 7)) (* 448 (^ x 6)) (* (- 896) (^ x 5)) (* 1120 (^ x 4)) (* (- 896) (^ x 3)) (* 448 (^ x 2)) (* (- 128) x) 16) 1))))
(check-sat)
Why is this happening? I guess the difference is that Z3 already knows some clauses and this keeps it from finding unsat.
Googling this issue, it seems like incremental solving is always good, so it seems weird that it has worse results here.
This is unfortunate, but not at all unexpected. Incremental mode uses different heuristics compared to the one-shot solver. The usual trick is to look at the verbose output (run it with -v:10 or similar), and see what internal tactics kick in. Of course, the verbose output can be hard to decipher, if not impossible. But it usually is indicative of where the solver gets "stuck."
Doing this, I was able to get it to terminate in the incremental case using the command:
(check-sat-using qfnra-nlsat)
instead of plain check-sat. Whether you should always use this is an interesting question. It's entirely problem specific. But the above incantation solves your current problem.
You might want to raise this as a question at https://github.com/Z3Prover/z3/discussions. Developers might have better advice for you.