blob: 4d87fdbae9cb49e7040a6025cdfce4391a2c35c2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
; COMMAND-LINE: --arith-brab -q
; COMMAND-LINE: --no-arith-brab -q
; EXPECT: sat
(set-logic ALL)
(declare-fun x1 () Real)
(declare-fun y1 () Real)
(declare-fun m1 () Real)
(declare-fun b1 () Real)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= y1 (+ b1 (* m1 x1))))
(assert (= x1 (/ m1 (- y1 b1))))
(assert (= b1 1.25))
(assert (= m1 (/ 1 3)))
(assert (and (> x x1) (> y y1)))
(check-sat)
(exit)
|
