File tree Expand file tree Collapse file tree 2 files changed +9
-2
lines changed Expand file tree Collapse file tree 2 files changed +9
-2
lines changed Original file line number Diff line number Diff line change 1
- CORE
1
+ KNOWNBUG
2
2
main.c
3
3
--unwind 2 --smt2 --outfile main.smt2
4
4
^EXIT=0$
5
5
^SIGNAL=0$
6
6
--
7
7
^Invalid expression: failed to get width of byte_update
8
+ --
9
+ 20220523: Marked as KNOWNBUG due to encoding into some solvers not being
10
+ done correctly. This works for z3 and cvc4, but not other solvers.
Original file line number Diff line number Diff line change 1
- CORE broken-smt-backend
1
+ KNOWNBUG broken-smt-backend
2
2
main.c
3
3
--smt2 --outfile -
4
4
\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)
@@ -11,6 +11,10 @@ main.c
11
11
\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
12
12
\(= \(select array\.3 \(_ bv\d+ 64\)\) false\)
13
13
--
14
+ 20220523: Marked as KNOWNBUG due to encoding into some solvers not being
15
+ done correctly. This works for z3 and cvc4, but not other solvers. Old
16
+ comments below.
17
+
14
18
This test checks for correctness of BitVec-array encoding of Boolean arrays.
15
19
16
20
Ideally, we shouldn't have to check the SMT output, but should run with backend
You can’t perform that action at this time.
0 commit comments