Skip to content

Commit babbd24

Browse files
committed
More details for bounds_check1 test failure
This isn't obviously failing, it just takes a long time.
1 parent a8420bb commit babbd24

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

regression/cbmc/bounds_check1/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-z3-smt-backend
1+
CORE thorough-smt-backend
22
main.c
33
--bounds-check --pointer-check
44
^EXIT=10$
@@ -12,3 +12,6 @@ payload\[\(.*\)[kl]2\]: FAILURE
1212
\[\(.*\)i\]: FAILURE
1313
dest\[\(.*\)j\]: FAILURE
1414
payload\[\(.*\)[kl]\]: FAILURE
15+
--
16+
Appears to take Z3 more than 10 minutes to solve, and approximately 500 seconds
17+
when using the in-tree SMT solver.

0 commit comments

Comments
 (0)