blob: f7e5a3a0425260956d4c0e6462b125f204833931 (
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
32
|
; EXPECT: unsat
(set-logic AUFBV)
(set-info :status unsat)
(set-info :category "crafted")
(declare-sort Element 0)
(declare-fun a1 () (Array (_ BitVec 8) Element))
(declare-fun a2 () (Array (_ BitVec 8) Element))
(declare-fun a3 () (Array (_ BitVec 8) Element))
(declare-fun a4 () (Array (_ BitVec 8) Element))
(declare-fun i2 () (_ BitVec 8))
(declare-fun i3 () (_ BitVec 8))
(declare-fun e1 () Element)
(declare-fun e2 () Element)
(assert (not (= e1 e2)))
(assert (= a3 (store a1 (_ bv3 8) e1)))
(assert (= a4 (store a2 (_ bv3 8) e1)))
(assert (= (select a3 (_ bv2 8)) e1))
(assert (= (select a4 (_ bv2 8)) e2))
; (assert (eqrange a3 a4 (_ bv0 8) (_ bv2 8)))
(assert (forall ((x (_ BitVec 8)))
(=> (and (bvule (_ bv0 8) x) (bvule x (_ bv2 8))) (= (select a3 x) (select a4 x)))
))
(check-sat)
(exit)
|
