From b47bb51e37ec7f4d4da081aa3deb510566faea9a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 17 Sep 2024 11:47:37 +0000
Subject: [PATCH] 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.
---
 .../dynamic-frames/dfcc_instrument_loop.cpp   | 36 +++++++++++++++----
 1 file changed, 30 insertions(+), 6 deletions(-)

diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp
index 20952a1c939..dfb0080c6ae 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp
+++ b/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);
+    }
   }
 
   {