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 71836bb commit 1cf3722Copy full SHA for 1cf3722
regression/cbmc-incr-oneloop/no-asserts/test.c
@@ -0,0 +1,7 @@
1
+int main() {
2
+ for(int i = 0; i < 10; ++i) {
3
+
4
+ }
5
+ // nothing to check
6
+ return 0;
7
+}
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
8
+--
9
+Incremental status
10
11
+Verify no incremental status updates when no properties to check
0 commit comments