[524] % z3release small.smt2
sat
ASSERTION VIOLATION
File: ../src/nlsat/nlsat_explain.cpp
Line: 1450
UNEXPECTED CODE WAS REACHED.
Z3 4.8.11.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[525] % 
[525] % cat small.smt2
(set-option :trace true)
(set-option :smt.random_seed 2)
(set-option :smt.threads 2)
(set-option :nlsat.minimize_conflicts true)
(set-option :smt.arith.nl.tangents false)
(set-option :rewriter.flat false)
(declare-const a Int)
(declare-const b Int)
(assert (<= (* a a) 1))
(assert (>= (mod (* a a) a) 1 b))
(check-sat)
(check-sat-using (then purify-arith ctx-solver-simplify))
[526] %