blob: b5a88700b348b54a580486bb3594157ecc9a4cad (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(set-info :status sat)
(set-logic QF_ABV)
(declare-const A (Array Bool Bool))
(declare-const B (Array Bool Bool))
(declare-const b1 Bool)
(declare-const b2 Bool)
(declare-const b3 Bool)
(declare-const b4 Bool)
(assert (= A (store B b1 b2)))
(assert (= b3 (select A (select B b2))))
(assert (=> b1 b2))
(assert (not (and b2 b3)))
(assert (=> b3 b1))
(assert (= b4 (select B b2)))
(assert (xor b4 b2))
(check-sat)
|
