Contracts/DFCC: split conjunctions in loop invariants

Emitting one assertion (and assumption) per conjunct simplifies
debugging when proving a loop invariant fails. It also appears to
improve performance when using Bitwuzla, taking one example from more
than 30 minutes down to 8 seconds. On the same example, performance
using Z3 was not substantially different.

Author: tautschnig

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

@@ -426,9 +426,21 @@ dfcc_instrument_loopt::add_step_instructions(
     dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
   {
     // Assume the loop invariant after havocing the state.
-    code_assumet assumption{invariant};
-    assumption.add_source_location() = loop_head_location;
-    converter.goto_convert(assumption, step_instrs, language_mode);
+    if(invariant.id() == ID_and)
+    {
+      for(const auto &op : invariant.operands())
+      {
+        code_assumet assumption{op};
+        assumption.add_source_location() = loop_head_location;
+        converter.goto_convert(assumption, step_instrs, language_mode);
+      }
+    }
+    else
+    {
+      code_assumet assumption{invariant};
+      assumption.add_source_location() = loop_head_location;
+      converter.goto_convert(assumption, step_instrs, language_mode);
+    }
   }
 
   {
@@ -507,9 +519,21 @@ void dfcc_instrument_loopt::add_body_instructions(
       id2string(check_location.get_function()) + "." +
       std::to_string(cbmc_loop_id));
     // Assume the loop invariant after havocing the state.
-    code_assertt assertion{invariant};
-    assertion.add_source_location() = check_location;
-    converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
+    if(invariant.id() == ID_and)
+    {
+      for(const auto &op : invariant.operands())
+      {
+        code_assertt assertion{op};
+        assertion.add_source_location() = check_location;
+        converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
+      }
+    }
+    else
+    {
+      code_assertt assertion{invariant};
+      assertion.add_source_location() = check_location;
+      converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
+    }
   }
 
   {