From d5b99941cbaa69b7fd9990159264a553e9fb4e49 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 30 Apr 2024 19:36:04 -0400
Subject: [PATCH] fixup: timeframe handles must be frozen

This is a fixup for 0158a8b102478b57ac19e217744bf8432.  This has returned a
conjunction of handles instead of a handle.  The conjunction isn't frozen,
and hence failed when using incremental SAT.
---
 regression/ebmc/SVA-LTL/freeze.desc | 9 +++++++++
 regression/ebmc/SVA-LTL/freeze.sv   | 5 +++++
 src/trans-word-level/property.cpp   | 4 ++--
 3 files changed, 16 insertions(+), 2 deletions(-)
 create mode 100644 regression/ebmc/SVA-LTL/freeze.desc
 create mode 100644 regression/ebmc/SVA-LTL/freeze.sv

diff --git a/regression/ebmc/SVA-LTL/freeze.desc b/regression/ebmc/SVA-LTL/freeze.desc
new file mode 100644
index 000000000..f14bf322f
--- /dev/null
+++ b/regression/ebmc/SVA-LTL/freeze.desc
@@ -0,0 +1,9 @@
+CORE
+freeze.sv
+--bound 1
+^\[main\.property\.p1\] always s_eventually main\.w: REFUTED$
+^\[main\.property\.p2\] always s_eventually !main\.w: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
diff --git a/regression/ebmc/SVA-LTL/freeze.sv b/regression/ebmc/SVA-LTL/freeze.sv
new file mode 100644
index 000000000..0a827caa4
--- /dev/null
+++ b/regression/ebmc/SVA-LTL/freeze.sv
@@ -0,0 +1,5 @@
+module main;
+  wire w;
+  p1: assert property (s_eventually w);
+  p2: assert property (s_eventually !w);
+endmodule
diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
index e9c7c356e..05d27932e 100644
--- a/src/trans-word-level/property.cpp
+++ b/src/trans-word-level/property.cpp
@@ -192,7 +192,7 @@ static void property_obligations_rec(
   {
     // current state property
     exprt tmp = instantiate(property_expr, current, no_timeframes, ns);
-    obligations[current].push_back(solver.handle(tmp));
+    obligations[current].push_back(tmp);
   }
 }
 
@@ -256,7 +256,7 @@ void property(
     DATA_INVARIANT(
       t >= 0 && t < no_timeframes, "obligation must have valid timeframe");
     auto t_int = numeric_cast_v<std::size_t>(t);
-    prop_handles[t_int] = conjunction(obligation_it.second);
+    prop_handles[t_int] = solver.handle(conjunction(obligation_it.second));
   }
 }