(purify-arith, ctx-solver-simplify) Soundness bug on QF_NIA formula

[muchang]

Hi,
For this case, Z3 gives an incorrect answer:

[539] % z3release small.smt2
unsat
sat
[540] % cat small.smt2
(declare-fun c () Int)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (> a 0 c (* a b)))
(assert (= b (div c a)))
(check-sat-using (then purify-arith ctx-solver-simplify))
(check-sat)
[541] %

OS: Ubuntu 18.04
Commit: ce07138

[levnach]

The debug build of ce07138 gives
./z3 ~/Dropbox/smts/4340.smt2
ASSERTION VIOLATION
File: ../../src/smt/tactic/ctx_solver_simplify_tactic.cpp
Line: 141
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

A lemma generated by intervals::check_nex() is incorrect. I am looking at it.
Fixed in aaf05f1