We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 3f6f0ca commit 4972f54Copy full SHA for 4972f54
regression/cbmc-incr-oneloop/no-asserts/test.c
@@ -0,0 +1,8 @@
1
+int main()
2
+{
3
+ for(int i = 0; i < 10; ++i)
4
+ {
5
+ }
6
+ // nothing to check
7
+ return 0;
8
+}
regression/cbmc-incr-oneloop/no-asserts/test.desc
@@ -0,0 +1,11 @@
+CORE
+test.c
+--incremental-loop main.0
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
9
+Incremental status
10
11
+Verify no incremental status updates when no properties to check
0 commit comments