Skip to content

Commit b8f6035

Browse files
committed
SMT conversion does not allow 0-sized arrays
so this test cannot be verified using smt-solver until smt conversion is fixed/extended.
1 parent 771bf6e commit b8f6035

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.i
33
--bounds-check --32 --no-simplify
44
^EXIT=10$

0 commit comments

Comments
 (0)