File: array_strange.basic

package info (click to toggle)
boolector 3.2.4-1
  • links: PTS, VCS
  • area: main
  • in suites: sid
  • size: 20,744 kB
  • sloc: ansic: 83,136; cpp: 18,159; sh: 3,668; python: 2,889; makefile: 210
file content (36 lines) | stat: -rw-r--r-- 528 bytes parent folder | download
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
0 rem write value i at indices i and check if array[i] == i
0 rem line 1070 buggy: 'eq' instead of 'ne' -> instance should be SAT
0 save a
110 rem read n
120 load 8
130 save n
170 load 0
175 save i
176 load i
177 ge n
178 jmp 1010
180 load a
185 add i
190 save w
200 load i
210 poke w
220 add 1
225 save i
230 goto 176
1000 rem check:
1010 load 0
1020 save i
1021 load i
1022 ge n
1023 jmp 1150
1030 load a
1040 add i
1050 save w
1060 peek w
1070 eq i
1080 jmp 1140
1090 add 1
1100 save i
1130 goto 1021
1140 exit 1
1150 exit 0