[754] % z3release small.smt2
sat
[755] % z3release smt.phase_selection=6 smt.threads=2 small.smt2
unsat
[756] % 
[756] % cat small.smt2
(set-logic QF_NIRA)
(declare-fun c () Real)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (<= 4 c))
(assert
 (or (<= (- a) (div (to_int c) (to_int a)))
 (<=
  (div (to_int b)
  (mod 4
   (to_int (/ a (* c (div (- 3) (to_int (* c c))))))))
  0)))
(assert (> a b))
(assert (> a c))
(check-sat)
[757] %