$ z3-4.8.10 small.smt2
sat
$ z3release small.smt2
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
$ cat small.smt2
(set-option :nlsat.minimize_conflicts true)
(set-option :nlsat.shuffle_vars true)
(set-option :nlsat.simplify_conflicts false)
(set-option :rewriter.push_ite_arith true)
(set-option :smt.arith.nl.order false)
(set-option :smt.arith.nl.tangents false)
(declare-const a Int)
(assert (>= (mod (div 531 (* 81 81 a a a)) a) (* (- a) a a a)))
(assert (< (* a a (- 81 (* 81 a a a a))) 0))
(check-sat)