Merge pull request #473 from diffblue/bmc-freeze

fixup: timeframe handles must be frozen

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$
+--
+--

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

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