blob: 67d2a09b73d7d4724b74d22327535a36c302e8db (
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
29
30
31
|
;; (set-logic QF_ALIA)
(set-logic QF_AUFBVLIA)
(declare-fun bv1 () (_ BitVec 32))
(declare-fun bv2 () (_ BitVec 32))
(declare-fun bv3 () (_ BitVec 32))
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun c () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun d () (Array (_ BitVec 32) (_ BitVec 32)))
(assert (= #b00000000000000000000000000000000 bv1))
(assert (= #b00000000000000000000000000000001 bv2))
(assert (= #b00000000000000000000000000000100 bv3))
(assert (not
(=> (= c (store b bv1 bv3))
(=> (= d (store (store b bv1 bv3) bv2 bv3))
(=> (= a (store d bv2 (select b bv2)))
(= a c))))))
(check-sat)
|
