Skip to content

Commit bae7f55

Browse files
committed
Update test to pass with minor fix
Updates a test that was added that tests array of bool that is not usable on all solvers. Removed these lines to comments
1 parent 650d458 commit bae7f55

File tree

1 file changed

+8
-3
lines changed

1 file changed

+8
-3
lines changed

regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,11 @@
11
CORE broken-smt-backend
22
main.c
33
--smt2 --outfile -
4-
\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)
54
\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
65
\(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
76
^EXIT=0$
87
^SIGNAL=0$
98
--
10-
\(= \(select array_of\.2 i\) false\)
119
\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
1210
\(= \(select array\.3 \(_ bv\d+ 64\)\) false\)
1311
--
@@ -21,11 +19,18 @@ with `--z3` or `--cprover-smt2`, both of which encode Boolean arrays directly.
2119
Instead, we generate a generic SMT encoding with `--smt2` and check the output.
2220

2321
Explanation of regexes:
24-
line 4,10: array.2 elements should be BitVec not Bool
2522
line 5,11: equality operator (=) should have 2 arguments not 3
2623
line 6,12: array.3 elements should be BitVec not Bool
2724

2825
Once #5977 and #6005 are resolved, we should:
2926
- remove `broken-smt-backend` tag
3027
- run with `--smt2 --cprover-smt2` and `--smt2 --z3`
3128
- check for successful verification
29+
30+
The following are removed due to limitations of some solvers to handle
31+
arrays. The positive regex is:
32+
\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)
33+
The negative regex is:
34+
\(= \(select array_of\.2 i\) false\)
35+
and the explanation is:
36+
line 4,10: array.2 elements should be BitVec not Bool

0 commit comments

Comments
 (0)