summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/int-real-univ.smt2
blob: e7d79bbf64bd2272f059ef3fc1e904e9029ea8fe (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

; COMMAND-LINE: --sets-ext
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)

(declare-fun a () (Set Real))

(declare-fun x () Real)

(assert (= (as univset (Set Real)) (as univset (Set Real))))

(assert (member x a))

(assert (and (<= 5.5 x) (< x 6.1)))

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