diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp
index bb51b478..c98d26c4 100644
--- a/src/ebmc/bdd_engine.cpp
+++ b/src/ebmc/bdd_engine.cpp
@@ -409,8 +409,8 @@ void bdd_enginet::compute_counterexample(
   auto netlist_property = netlist.properties.find(property.identifier);
   CHECK_RETURN(netlist_property != netlist.properties.end());
 
-  ::unwind_property(
-    netlist_property->second, bmc_map, property.timeframe_literals);
+  property.timeframe_literals =
+    ::unwind_property(netlist_property->second, bmc_map);
 
   // we need the propertyt to fail in one of the timeframes
   bvt clause=property.timeframe_literals;
diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp
index ebaa553a..f20bdc3a 100644
--- a/src/ebmc/bmc.cpp
+++ b/src/ebmc/bmc.cpp
@@ -228,13 +228,8 @@ void bmc(
       continue;
     }
 
-    ::property(
-      property.normalized_expr,
-      property.timeframe_handles,
-      message_handler,
-      solver,
-      bound + 1,
-      ns);
+    property.timeframe_handles = ::property(
+      property.normalized_expr, message_handler, solver, bound + 1, ns);
 
     // If it's an assumption, then add it as constraint.
     if(property.is_assumed())
diff --git a/src/ebmc/cegar/bmc_cegar.cpp b/src/ebmc/cegar/bmc_cegar.cpp
index dfd8db4e..5ef020bd 100644
--- a/src/ebmc/cegar/bmc_cegar.cpp
+++ b/src/ebmc/cegar/bmc_cegar.cpp
@@ -78,7 +78,7 @@ void bmc_cegart::unwind(
   for(auto &property_it : netlist.properties)
   {
     auto &prop_bv = prop_bv_map[property_it.first];
-    unwind_property(property_it.second, bmc_map, prop_bv);
+    prop_bv = unwind_property(property_it.second, bmc_map);
 
     disjuncts.push_back(!solver.land(prop_bv));
   }
diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp
index 833392ad..25967f29 100644
--- a/src/ebmc/property_checker.cpp
+++ b/src/ebmc/property_checker.cpp
@@ -255,8 +255,8 @@ property_checker_resultt bit_level_bmc(
       auto netlist_property = netlist.properties.find(property.identifier);
       CHECK_RETURN(netlist_property != netlist.properties.end());
 
-      ::unwind_property(
-        netlist_property->second, bmc_map, property.timeframe_literals);
+      property.timeframe_literals =
+        ::unwind_property(netlist_property->second, bmc_map);
 
       if(property.is_assumed())
       {
diff --git a/src/trans-netlist/unwind_netlist.cpp b/src/trans-netlist/unwind_netlist.cpp
index d52c067c..b227e6d6 100644
--- a/src/trans-netlist/unwind_netlist.cpp
+++ b/src/trans-netlist/unwind_netlist.cpp
@@ -141,14 +141,14 @@ Function: unwind_property
 
 \*******************************************************************/
 
-void unwind_property(
+bvt unwind_property(
   const netlistt::propertyt &property,
-  const bmc_mapt &bmc_map,
-  bvt &prop_bv)
+  const bmc_mapt &bmc_map)
 {
   PRECONDITION(std::holds_alternative<netlistt::Gpt>(property));
   auto property_node = std::get<netlistt::Gpt>(property).p;
 
+  bvt prop_bv;
   prop_bv.resize(bmc_map.timeframe_map.size());
 
   for(std::size_t t = 0; t < bmc_map.timeframe_map.size(); t++)
@@ -156,6 +156,8 @@ void unwind_property(
     literalt l=bmc_map.translate(t, property_node);
     prop_bv[t]=l;
   }
+
+  return prop_bv;
 }
 
 /*******************************************************************\
diff --git a/src/trans-netlist/unwind_netlist.h b/src/trans-netlist/unwind_netlist.h
index 5d01b081..b3fb4602 100644
--- a/src/trans-netlist/unwind_netlist.h
+++ b/src/trans-netlist/unwind_netlist.h
@@ -36,9 +36,6 @@ void unwind(
 bool netlist_bmc_supports_property(const class exprt &);
 
 // unwind a netlist property
-void unwind_property(
-  const netlistt::propertyt &,
-  const bmc_mapt &,
-  bvt &prop_bv);
+bvt unwind_property(const netlistt::propertyt &, const bmc_mapt &);
 
 #endif
diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
index 70acd2fb..daef9da4 100644
--- a/src/trans-word-level/property.cpp
+++ b/src/trans-word-level/property.cpp
@@ -682,9 +682,8 @@ Function: property
 
 \*******************************************************************/
 
-void property(
+exprt::operandst property(
   const exprt &property_expr,
-  exprt::operandst &prop_handles,
   message_handlert &message_handler,
   decision_proceduret &solver,
   std::size_t no_timeframes,
@@ -696,7 +695,7 @@ void property(
   auto obligations = property_obligations(property_expr, no_timeframes);
 
   // Map obligations onto timeframes.
-  prop_handles.clear();
+  exprt::operandst prop_handles;
   prop_handles.resize(no_timeframes, true_exprt());
   for(auto &obligation_it : obligations.map)
   {
@@ -706,4 +705,6 @@ void property(
     auto t_int = numeric_cast_v<std::size_t>(t);
     prop_handles[t_int] = solver.handle(conjunction(obligation_it.second));
   }
+
+  return prop_handles;
 }
diff --git a/src/trans-word-level/property.h b/src/trans-word-level/property.h
index 1bff3522..64d6feae 100644
--- a/src/trans-word-level/property.h
+++ b/src/trans-word-level/property.h
@@ -16,9 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <solvers/decision_procedure.h>
 
-void property(
+exprt::operandst property(
   const exprt &property_expr,
-  exprt::operandst &prop_handles,
   message_handlert &,
   decision_proceduret &solver,
   std::size_t no_timeframes,