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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
(declare-const s State)
(declare-const t Index)
(declare-const other Index)
(declare-const a Index)
(declare-const v Word)
(declare-const r Index)
(declare-const destination Index)
(assert (bvult t #x02))
(assert (bvult other #x02))
(assert (bvult a #x10))
(assert (bvult r #x04))
(assert (bvule (at (heads s) t) (at (tails s) t)))
(assert (bvult (at (tails s) t) #x40))
(assert (bvult (pending s t) #x08))
(assert (distinct other t))
(push 1)
(assert (distinct (read (write s t a v) t a) v))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (memory (write s t a v)) (memory s)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (pending (write s t a v) t) (bvadd (pending s t) #x01)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (pending (write s t a v) other) (pending s other)))
(check-sat)
(pop 1)
(push 1)
(assert (bvugt (pending s t) #x00))
(assert (distinct (pending (drain s t) t) (bvsub (pending s t) #x01)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (pending (drain s t) other) (pending s other)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (reg (put s t r v) t r) v))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (pc (advance s t destination) t) destination))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (pc (advance s t destination) other) (pc s other)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (at (critical (mark s t #x01)) t) #x01))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (at (memory (exchange s t a r v)) a) v))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (reg (exchange s t a r v) t r) (at (memory s) a)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (reg (load-step s t a r) t r) (read s t a)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (memory (load-step s t a r)) (memory s)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (pending (fence-step s t) t) (pending s t)))
(check-sat)
(pop 1)
(push 1)
(assert (= (pending s t) #x00))
(assert (distinct (at (memory (store-step s t a v true)) a) v))
(check-sat)
(pop 1)
|