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));
   }
 }