Issues with tactics

[merlinsun]

Hi,
For this following instance, z3 returns unsat with check-sat-using (then nnf nlsat), while returns sat with check-sat.
QF_NIA.zip

Commit: dd91cfb

[merlinsun]

This is a simplified case:

(declare-fun a__17 () Int)
(declare-fun a__3 () Int)
(declare-fun a__8 () Int)
(declare-fun b__21 () Int)
(declare-fun b__18 () Int)
(declare-fun a__10 () Int)
(declare-fun a__15 () Int)
(declare-fun b__19 () Int)
(declare-fun a__14 () Int)
(declare-fun a__12 () Int)
(declare-fun a__16 () Int)
(declare-fun a__6 () Int)
(declare-fun a__13 () Int)
(declare-fun a__4 () Int)
(declare-fun a__9 () Int)
(declare-fun a__11 () Int)
(declare-fun b__20 () Int)
(declare-fun a__5 () Int)
(declare-fun a__7 () Int)
(declare-fun a__2 () Int)
(assert
 (not (not (= (+ a__3 a__17) 10))))
(assert
 (not (not (= (+ a__3 a__17) 10))))
(assert
 (let (($x26 (>= (+ 1 (* (- 0 1) b__18)) 0)))
 (let (($x85 (>= (+ (* b__18 a__10) (* (- 0 1) b__18)) 0)))
 (let (($x113 (and $x85 $x26 (= (+ (+ (* 84 b__21) (* 38 a__8)) 5624) 5624))))
 (let ((?x99 (* b__19 a__15)))
 (let ((?x66 (- 0 1)))
 (let ((?x92 (* ?x66 ?x99)))
 (let ((?x39 (* b__19 a__12)))
 (let (($x43 (>= (+ ?x39 (* b__19 a__15 a__14) ?x92) 0)))
 (let (($x138 (>= a__17 0)))
 (let (($x192 (>= a__16 0)))
 (let (($x82 (>= a__6 0)))
 (let (($x187 (>= a__13 0)))
 (let (($x155 (>= a__14 0)))
 (let (($x28 (>= a__15 0)))
 (let (($x151 (>= a__12 0)))
 (let (($x164 (>= a__4 0)))
 (let (($x165 (>= a__9 0)))
 (let (($x198 (>= a__11 0)))
 (let (($x10 (>= a__10 0)))
 (let (($x7 (>= b__21 0)))
 (let (($x9 (>= 1 b__20)))
 (let (($x11 (>= b__20 0)))
 (let (($x109 (>= a__5 0)))
 (let (($x79 (>= a__3 0)))
 (let (($x248 (>= a__8 0)))
 (let (($x145 (>= b__19 0)))
 (let (($x55 (>= a__7 0)))
 (let (($x195 (>= a__2 0)))
 (let (($x204 (>= 1 b__18)))
 (let (($x104 (>= b__18 0)))
 (let ((?x50 (+ (* a__5 a__3) (* ?x66 (* a__11 a__7 a__2)) (* ?x66 (* a__14 a__8 a__2)) (* ?x66 (* a__14 a__5 a__3)))))
 (let ((?x86 (+ (* a__5 a__2) (* ?x66 (* a__10 a__7 a__2)) (* ?x66 (* a__13 a__8 a__2)) (* ?x66 (* a__13 a__5 a__3)))))
 (let (($x29 (>= ?x86 0)))
 (let ((?x222 (* a__4 a__2)))
 (let ((?x75 (+ ?x222 (* ?x66 (* a__6 a__2)) (* ?x66 (* a__9 a__7 a__2)) (* ?x66 (* a__12 a__8 a__2)) (* ?x66 (* a__12 a__5 a__3)) ?x66)))
 (let ((?x21 (* b__21 a__5 a__17)))
 (let ((?x140 (* b__21 a__16)))
 (let ((?x100 (+ ?x140 (* b__21 a__4 a__17) (* ?x66 (* b__21 a__4)) (* ?x66 (* b__21 a__4 a__5)) (* ?x66 (* b__21 a__16 a__5 a__5)))))
 (let ((?x163 (+ (* b__20 a__5 a__8) (* ?x66 (* b__20 a__17 a__8 a__5)))))
 (let ((?x197 (+ (* b__20 a__6) (* b__20 a__4 a__7) (* b__20 a__4 a__8) (* ?x66 (* b__20 a__4)) (* ?x66 (* b__20 a__6 a__5)) (* ?x66 (* b__20 a__16 a__8 a__5)))))
 (let (($x95 (>= (+ (* b__20 a__7) (* ?x66 b__20)) 0)))
 (let ((?x220 (+ ?x39 (* b__19 a__4 a__13) (* b__19 a__4 a__14) (* ?x66 (* b__19 a__4)) (* ?x66 (* b__19 a__12 a__5)))))
 (let (($x96 (>= ?x220 0)))
 (let ((?x193 (+ (* b__18 a__9) (* b__18 a__4 a__10) (* b__18 a__4 a__11) (* ?x66 (* b__18 a__4)) (* ?x66 (* b__18 a__9 a__5)))))
 (let ((?x89 (+ (* b__21 a__2 a__8 a__5) (* ?x66 (* a__2 a__8 a__5)))))
 (let (($x189 (= ?x89 0)))
 (let (($x111 (= (+ (* b__20 a__2) (* ?x66 a__2)) 0)))
 (let (($x225 (and $x26 (= (+ (* b__18 a__2 a__7) (* ?x66 (* a__2 a__7))) 0) (>= (+ 1 (* ?x66 b__19)) 0) (= (+ (* b__19 a__2 a__8) (* ?x66 (* a__2 a__8))) 0) (= (+ (* b__19 a__3 a__5) (* ?x66 (* a__3 a__5))) 0) (>= (+ 1 (* ?x66 b__20)) 0) $x111 (>= (+ 1 (* ?x66 b__21)) 0) $x189 $x85 (>= (+ (* b__18 a__11) (* ?x66 b__18)) 0) (>= ?x193 0) $x43 (>= (+ ?x39 (* b__19 a__15 a__13) ?x92) 0) $x96 $x95 (>= ?x197 0) (>= ?x163 0) (>= ?x100 0) (>= (+ ?x21 (* ?x66 (* b__21 a__17 a__5 a__5))) 0) (>= (+ (* b__21 a__17) (* ?x66 b__21)) 0) (>= ?x75 0) $x29 (>= ?x50 0) $x104 $x204 $x195 $x55 $x145 (>= 1 b__19) $x248 $x79 $x109 $x11 $x9 $x7 (>= 1 b__21) $x10 $x198 $x165 $x164 $x151 $x28 $x155 $x187 $x82 $x192 $x138)))
 (let (($x98 (= (* a__16 a__12) 0)))
 (let (($x34 (= (* a__12 a__12) 0)))
 (let (($x149 (and $x113 $x95 (= (+ (+ (* 82 a__7) (* 97 a__15)) 4925) 5007))))
 (let (($x40 (and $x149 (and $x111 (and $x9 $x96 (= (+ a__3 a__17) 10)) $x34) $x98)))
 (let (($x53 (and (and $x189 (and $x138 $x29 (= (* a__9 a__9) 4)) $x34) $x40 (= (+ (+ (* 42 b__19) (* 43 a__9)) 9739) 9867))))
 (let (($x182 (and (and $x138 $x204 (= (+ a__3 a__17) 10)) $x138 (= (+ (+ b__21 a__16) 9944) 9953))))
 (let (($x244 (and (not (not (and $x182 $x53 $x98))) (and (and (and $x145 $x225) $x43) $x113))))
 (not (not $x244))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert
 (not (not (= (+ a__3 a__17) 10))))
(check-sat-using (then nnf nlsat))

[NikolajBjorner]

nlsat related bugs are most likely duplicates or variants of #2650

[merlinsun]

nlsat related bugs are most likely duplicates or variants of #2650

Thanks, Nikolaj.
I will try to avoid duplicate reports in the future.