[615] % cvc4 small.smt2
sat
[616] % z3-4.8.7 small.smt2
unknown
[617] % 
[617] % cvc4 small.smt2
sat
[618] % z3 small.smt2
unsat
[619] % cat small.smt2
(set-logic QF_NIRA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(assert (<= (/ 2 f b) g))
(assert (<= (* g a (* a d)) (- 2)))
(assert (<= (+ b (* 6 e) (* (- 25) c)) (+ h h (* (- 11) g)) 5))
(check-sat)
[620] %