1 sort bitvec 1
5 sort bitvec 5
23 sort bitvec 32
; Symbolic Constant: addr
121 state 5 addr
122 next 5 121 121
; Symbolic Constant: data
123 state 23 data
124 next 23 123 123
; Symbolic Constant: mem
125 sort array 5 23
126 state 125 mem
127 next 125 126 126
; mem[addr := data]
148 write 125 126 121 123
; mem_n = mem[addr := data]
155 state 125 mem_n
156 init 125 155 148
157 next 125 155 155
; bad: mem_n[a] != mem[a]
; Symbolic Constant: a
200 state 5 a
201 next 5 200 200
210 read 23 126 200
211 read 23 155 200
212 neq 1 210 211
213 bad 212