Skip to content

Commit 52c3eed

Browse files
Test that goal disjunction clauses are output
Previously the assertion clause set was empty in this case.
1 parent 5b51606 commit 52c3eed

File tree

2 files changed

+2
-0
lines changed

2 files changed

+2
-0
lines changed

regression/solver-hardness/solver-hardness-simple/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,6 @@ int main()
55
int a;
66
int b;
77
assert(a + b < 10);
8+
assert(a < 10);
89
return 0;
910
}

regression/solver-hardness/solver-hardness-simple/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,6 @@ main.c
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
77
\"SAT_hardness\":\{(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+),(\"ClauseSet\":\[.*\]|\"Clauses\":\d+|\"Variables\":\d+|\"Literals\":\d+)\}
8+
\"GOTO_ID\":32,\"SAT_hardness\":\{\"ClauseSet\":\[.*,571\],\"Clauses\":571
89
--
910
^warning: ignoring

0 commit comments

Comments
 (0)