blob: 9519e89a1b30a5df485f90ddc26a626b051300c3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
; COMMAND-LINE: --miplib-trick
; EXPECT: sat
(set-logic ALL)
(set-option :incremental false)
(declare-fun tmp1 () Int)
(declare-fun tmp2 () Int)
(declare-fun tmp3 () Int)
(declare-fun tmp4 () Int)
(declare-fun x () Bool)
(declare-fun y () Bool)
(declare-fun z () Bool)
(assert (=> (and (not x) (and (not y) true)) (= tmp1 0)))
(assert (=> (and x (and (not y) true)) (= tmp1 4)))
(assert (=> (and (not x) (and y true)) (= tmp1 6)))
(assert (=> (and x (and y true)) (= tmp1 10)))
(assert (=> (and (not x) (and (not z) true)) (= tmp2 0)))
(assert (=> (and x (and (not z) true)) (= tmp2 2)))
(assert (=> (and (not x) (and z true)) (= tmp2 9)))
(assert (=> (and x (and z true)) (= tmp2 11)))
(assert (=> (and (not y) (and (not z) true)) (= tmp3 0)))
(assert (=> (and y (and (not z) true)) (= tmp3 5)))
(assert (=> (and (not y) (and z true)) (= tmp3 16)))
(assert (=> (and y (and z true)) (= tmp3 21)))
(assert (=> (and (not x) (and (not y) true)) (= tmp4 0)))
(assert (=> (and x (and (not y) true)) (= tmp4 4)))
(assert (=> (and (not x) (and y true)) (= tmp4 6)))
(assert (=> (and x (and y true)) (= tmp4 10)))
(check-sat)
|
