Skip to content

Commit 7a3d072

Browse files
committed
Add comment to test that assert was required to expose fixpoint error.
We could not reproduce the error with branching or goblint_check.
1 parent f947dcc commit 7a3d072

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

tests/regression/37-congruence/16-refinement-fixpoint.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ int main(void)
1313
d += 2U;
1414

1515
e += 3U;
16-
16+
// To produce the fixpoint not reached error, the following needed to be an assert:
1717
assert(e == (unsigned int )c + d); //UNKNOWN
1818

1919
burgo = 23;

0 commit comments

Comments
 (0)