Incremental solving producing cprover status as it goes

regression/cbmc-incr-oneloop/alarm1/test.desc

@@ -1,8 +1,10 @@
 CORE
 main.c
 --incremental-loop main.0 --unwind-max 15
+activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 15
 --
 ^warning: ignoring

regression/cbmc-incr-oneloop/alarm2/test-json-output.desc

@@ -5,5 +5,6 @@ main.c
 ^SIGNAL=0$
 "messageText": "VERIFICATION FAILED"
 "currentUnwinding": 1
+"incrementalStatus": "INCONCLUSIVE"
 --
 ^warning: ignoring

regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc

@@ -6,5 +6,6 @@ main.c
 <text>VERIFICATION FAILED</text>
 <current-unwinding>1</current-unwinding>
 <refinement-iteration>1</refinement-iteration>
+<incremental-status>INCONCLUSIVE</incremental-status>
 --
 ^warning: ignoring

regression/cbmc-incr-oneloop/alarm2/test.desc

@@ -1,9 +1,15 @@
 CORE
 main.c
 --incremental-loop main.0 --unwind-min 5 --unwind-max 10
+activate-multi-line-match
 Current unwinding: 1
+Incremental status: INCONCLUSIVE
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 6
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 7
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+--
+The multi-line match is added to verify that an incremental status is printed immediately after each unwinding

regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc

@@ -0,0 +1,18 @@
+CORE
+test.c
+--incremental-loop main.0 --no-propagation
+activate-multi-line-match
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 2
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 6
+Incremental status: FAILURE\nCurrent unwinding: 7
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Ensure that with multiple properties, the incremental status
+switches to failure as soon as one property has been falsified
+but keeps unwinding till it has resolved them all
+
+Use `--no-propagation` to ensure that even the output is the same regardless of whether the asserts are checked via the solver or the constant propagator

regression/cbmc-incr-oneloop/multiple-asserts/test.c

@@ -0,0 +1,9 @@
+int main()
+{
+  for(int i = 0; i < 10; ++i)
+  {
+    assert(i != 5);
+    assert(i != 8);
+  }
+  return 0;
+}

regression/cbmc-incr-oneloop/multiple-asserts/test.desc

@@ -0,0 +1,16 @@
+CORE
+test.c
+--incremental-loop main.0
+activate-multi-line-match
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 2
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 6
+Incremental status: FAILURE\nCurrent unwinding: 7
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Ensure that with multiple properties, the incremental status
+switches to failure as soon as one property has been falsified
+but keeps unwinding till it has resolved them all

regression/cbmc-incr-oneloop/no-asserts/test.c

@@ -0,0 +1,8 @@
+int main()
+{
+  for(int i = 0; i < 10; ++i)
+  {
+  }
+  // nothing to check
+  return 0;
+}

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
+--
+Incremental status
+--
+Verify no incremental status updates when no properties to check

regression/cbmc-incr-oneloop/valid-asserts/test.c

@@ -0,0 +1,8 @@
+int main()
+{
+  for(int i = 0; i < 10; ++i)
+  {
+    assert(i != 10);
+  }
+  return 0;
+}

regression/cbmc-incr-oneloop/valid-asserts/test.desc

@@ -0,0 +1,16 @@
+CORE
+test.c
+--incremental-loop main.0
+activate-multi-line-match
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 2
+Incremental status: INCONCLUSIVE\nCurrent unwinding: 10
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+Incremental status: SUCCESS
+--
+Check that for valid asserts, the incremental status is inconclusive
+as it is only after the incrementer has been stopped we conclude is
+verified.

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -47,6 +47,23 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
     prop_conv_solver->set_all_frozen();
 }
 
+void output_incremental_status(
+  const propertiest &properties,
+  messaget &message_hander)
+{
+  const auto any_failures = std::any_of(
+    properties.begin(),
+    properties.end(),
+    [](const std::pair<irep_idt, property_infot> &property) {
+      return property.second.status == property_statust::FAIL;
+    });
+  std::string status = any_failures ? "FAILURE" : "INCONCLUSIVE";
+  structured_datat incremental_status{
+    {{labelt({"incremental", "status"}),
+      structured_data_entryt::data_node(json_stringt(status))}}};
+  message_hander.statistics() << incremental_status;
+}
+
 incremental_goto_checkert::resultt single_loop_incremental_symex_checkert::
 operator()(propertiest &properties)
 {
@@ -152,6 +169,8 @@ operator()(propertiest &properties)
       break;
     }
 
+    output_incremental_status(properties, log);
+
     // We continue symbolic execution
     full_equation_generated =
       !symex.resume(goto_symext::get_goto_function(goto_model));