summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sets/comp-odd.smt2
blob: 1b1a13b345fba7991e297d9b5e41cdc7f7fcc6e7 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

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

(declare-fun x () (Set Int))

(assert (subset x (comprehension ((z Int)) true (* 2 z))))

(declare-fun a () Int)
(declare-fun b () Int)

(assert (= a (+ (* 8 b) 1)))
(assert (member a x))

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