test/regress/regress0/arith/bug569.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14

; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
; EXPECT: unsat
(set-logic QF_AUFLIRA)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun v1 () Int)
(declare-fun v3 () Int)
(declare-fun v5 () Real)
(assert (= (to_real v1) (+ (to_real v3) v5)))
(assert (< v5 1))
(assert (> v5 0))
(check-sat)
(exit)