summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arith/arith-tighten-1.smt2
blob: a8a5234a0b4d509b3e76028a82c2a217a6a0c14b (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

; COMMAND-LINE: --no-check-unsat-cores
; EXPECT: unsat
(set-logic QF_LIRA)

(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun x () Real)
(declare-fun y () Real)



(assert (= x y))
(assert (= x (- 2.5 y)))
(assert (>= (+ i j) x))
(assert (<= j (+ x 0.5)))
(assert (<= i 0))

(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback