diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp
index f18b9e4c0..c90b73b4c 100644
--- a/src/ebmc/k_induction.cpp
+++ b/src/ebmc/k_induction.cpp
@@ -261,7 +261,7 @@ void k_inductiont::induction_step()
         const exprt &p = to_unary_expr(property.normalized_expr).op();
         for(std::size_t c = 0; c < no_timeframes; c++)
         {
-          exprt tmp = instantiate(p, c, no_timeframes, ns);
+          exprt tmp = instantiate(p, c, no_timeframes);
           solver.set_to_true(tmp);
         }
       }
@@ -272,15 +272,13 @@ void k_inductiont::induction_step()
     // assumption: time frames 0,...,k-1
     for(std::size_t c = 0; c < no_timeframes - 1; c++)
     {
-      exprt tmp=
-        instantiate(p, c, no_timeframes-1, ns);
+      exprt tmp = instantiate(p, c, no_timeframes - 1);
       solver.set_to_true(tmp);
     }
     
     // property: time frame k
     {
-      exprt tmp=
-        instantiate(p, no_timeframes-1, no_timeframes, ns);
+      exprt tmp = instantiate(p, no_timeframes - 1, no_timeframes);
       solver.set_to_false(tmp);
     }
 
diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp
index 67c17bdd4..68ef7b420 100644
--- a/src/ebmc/random_traces.cpp
+++ b/src/ebmc/random_traces.cpp
@@ -478,8 +478,7 @@ void random_tracest::freeze(
   {
     for(auto &symbol : symbols)
     {
-      auto symbol_in_timeframe =
-        instantiate(symbol, i, number_of_timeframes, ns);
+      auto symbol_in_timeframe = instantiate(symbol, i, number_of_timeframes);
       (void)solver.handle(symbol_in_timeframe);
     }
   }
@@ -508,7 +507,7 @@ std::vector<exprt> random_tracest::random_input_constraints(
   {
     for(auto &input : inputs)
     {
-      auto input_in_timeframe = instantiate(input, i, number_of_timeframes, ns);
+      auto input_in_timeframe = instantiate(input, i, number_of_timeframes);
       auto constraint =
         equal_exprt(input_in_timeframe, random_value(input.type()));
       result.push_back(constraint);
@@ -538,7 +537,7 @@ std::vector<exprt> random_tracest::random_initial_state_constraints(
 
   for(auto &symbol : state_variables)
   {
-    auto symbol_in_timeframe = instantiate(symbol, 0, 1, ns);
+    auto symbol_in_timeframe = instantiate(symbol, 0, 1);
     auto constraint =
       equal_exprt(symbol_in_timeframe, random_value(symbol.type()));
     result.push_back(std::move(constraint));
diff --git a/src/ebmc/ranking_function.cpp b/src/ebmc/ranking_function.cpp
index da002618c..23a4b218c 100644
--- a/src/ebmc/ranking_function.cpp
+++ b/src/ebmc/ranking_function.cpp
@@ -171,14 +171,13 @@ std::pair<tvt, std::optional<trans_tracet>> is_ranking_function(
   // c) p holds in timeframe 1
 
   exprt ranking_function_decreases = less_than_exprt(
-    instantiate(ranking_function, 1, 2, ns),
-    instantiate(ranking_function, 0, 2, ns));
+    instantiate(ranking_function, 1, 2), instantiate(ranking_function, 0, 2));
   solver.set_to_false(ranking_function_decreases);
 
-  exprt p_at_0 = instantiate(p, 0, 2, ns);
+  exprt p_at_0 = instantiate(p, 0, 2);
   solver.set_to_false(p_at_0);
 
-  exprt p_at_1 = instantiate(p, 1, 2, ns);
+  exprt p_at_1 = instantiate(p, 1, 2);
   solver.set_to_false(p_at_1);
 
   decision_proceduret::resultt dec_result = solver();
diff --git a/src/trans-word-level/counterexample_word_level.cpp b/src/trans-word-level/counterexample_word_level.cpp
index 47bbd39be..49a379fbf 100644
--- a/src/trans-word-level/counterexample_word_level.cpp
+++ b/src/trans-word-level/counterexample_word_level.cpp
@@ -6,15 +6,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <iostream>
+#include "counterexample_word_level.h"
+
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 #include <langapi/language_util.h>
+#include <solvers/decision_procedure.h>
 
 #include "instantiate_word_level.h"
-#include "counterexample_word_level.h"
 
-#include <util/std_expr.h>
-#include <util/symbol_table.h>
+#include <iostream>
 
 /*******************************************************************\
 
diff --git a/src/trans-word-level/instantiate_word_level.cpp b/src/trans-word-level/instantiate_word_level.cpp
index ee32a69d9..67563afac 100644
--- a/src/trans-word-level/instantiate_word_level.cpp
+++ b/src/trans-word-level/instantiate_word_level.cpp
@@ -72,8 +72,8 @@ symbol_exprt timeframe_symbol(const mp_integer &timeframe, symbol_exprt src)
 class wl_instantiatet
 {
 public:
-  wl_instantiatet(const mp_integer &_no_timeframes, const namespacet &_ns)
-    : no_timeframes(_no_timeframes), ns(_ns)
+  explicit wl_instantiatet(const mp_integer &_no_timeframes)
+    : no_timeframes(_no_timeframes)
   {
   }
 
@@ -86,7 +86,6 @@ class wl_instantiatet
 
 protected:
   const mp_integer &no_timeframes;
-  const namespacet &ns;
 
   [[nodiscard]] std::pair<mp_integer, exprt>
   instantiate_rec(exprt, const mp_integer &t) const;
@@ -145,7 +144,7 @@ wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
   {
     // sequence expressions -- these may have multiple potential
     // match points, and evaluate to true if any of them matches
-    const auto match_points = instantiate_sequence(expr, t, no_timeframes, ns);
+    const auto match_points = instantiate_sequence(expr, t, no_timeframes);
     exprt::operandst disjuncts;
     disjuncts.reserve(match_points.size());
     mp_integer max = t;
@@ -228,10 +227,9 @@ Function: instantiate
 exprt instantiate(
   const exprt &expr,
   const mp_integer &t,
-  const mp_integer &no_timeframes,
-  const namespacet &ns)
+  const mp_integer &no_timeframes)
 {
-  wl_instantiatet wl_instantiate(no_timeframes, ns);
+  wl_instantiatet wl_instantiate(no_timeframes);
   return wl_instantiate(expr, t).second;
 }
 
@@ -250,9 +248,8 @@ Function: instantiate_property
 std::pair<mp_integer, exprt> instantiate_property(
   const exprt &expr,
   const mp_integer &current,
-  const mp_integer &no_timeframes,
-  const namespacet &ns)
+  const mp_integer &no_timeframes)
 {
-  wl_instantiatet wl_instantiate(no_timeframes, ns);
+  wl_instantiatet wl_instantiate(no_timeframes);
   return wl_instantiate(expr, current);
 }
diff --git a/src/trans-word-level/instantiate_word_level.h b/src/trans-word-level/instantiate_word_level.h
index 8ff13c927..9f18e9cf4 100644
--- a/src/trans-word-level/instantiate_word_level.h
+++ b/src/trans-word-level/instantiate_word_level.h
@@ -10,21 +10,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_BMC_INSTANTIATE_WORD_LEVEL_H
 
 #include <util/mp_arith.h>
-#include <util/namespace.h>
-
-#include <solvers/prop/prop_conv.h>
+#include <util/std_expr.h>
 
 exprt instantiate(
   const exprt &expr,
   const mp_integer &current,
-  const mp_integer &no_timeframes,
-  const namespacet &);
+  const mp_integer &no_timeframes);
 
 std::pair<mp_integer, exprt> instantiate_property(
   const exprt &,
   const mp_integer &current,
-  const mp_integer &no_timeframes,
-  const namespacet &);
+  const mp_integer &no_timeframes);
 
 std::string
 timeframe_identifier(const mp_integer &timeframe, const irep_idt &identifier);
diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
index fc2e492ea..c6b54c596 100644
--- a/src/trans-word-level/property.cpp
+++ b/src/trans-word-level/property.cpp
@@ -157,7 +157,6 @@ Function: property_obligations_rec
 
 static obligationst property_obligations_rec(
   const exprt &property_expr,
-  decision_proceduret &solver,
   const mp_integer &current,
   const mp_integer &no_timeframes,
   const namespacet &ns)
@@ -184,8 +183,7 @@ static obligationst property_obligations_rec(
 
     for(mp_integer c = current; c < no_timeframes; ++c)
     {
-      obligations.add(
-        property_obligations_rec(phi, solver, c, no_timeframes, ns));
+      obligations.add(property_obligations_rec(phi, c, no_timeframes, ns));
     }
 
     return obligations;
@@ -214,8 +212,7 @@ static obligationst property_obligations_rec(
 
     for(mp_integer u = current + lower; u <= current + upper; ++u)
     {
-      auto obligations_rec =
-        property_obligations_rec(op, solver, u, no_timeframes, ns);
+      auto obligations_rec = property_obligations_rec(op, u, no_timeframes, ns);
       disjuncts.push_back(obligations_rec.conjunction().second);
     }
 
@@ -247,8 +244,7 @@ static obligationst property_obligations_rec(
 
         for(mp_integer j = current; j <= k; ++j)
         {
-          auto tmp =
-            property_obligations_rec(phi, solver, j, no_timeframes, ns);
+          auto tmp = property_obligations_rec(phi, j, no_timeframes, ns);
           disjuncts.push_back(tmp.conjunction().second);
         }
 
@@ -293,8 +289,8 @@ static obligationst property_obligations_rec(
 
     for(mp_integer c = from; c <= to; ++c)
     {
-      auto tmp = property_obligations_rec(phi, solver, c, no_timeframes, ns)
-                   .conjunction();
+      auto tmp =
+        property_obligations_rec(phi, c, no_timeframes, ns).conjunction();
       time = std::max(time, tmp.first);
       disjuncts.push_back(tmp.second);
     }
@@ -342,8 +338,7 @@ static obligationst property_obligations_rec(
 
     for(mp_integer c = from; c <= to; ++c)
     {
-      obligations.add(
-        property_obligations_rec(phi, solver, c, no_timeframes, ns));
+      obligations.add(property_obligations_rec(phi, c, no_timeframes, ns));
     }
 
     return obligations;
@@ -368,7 +363,7 @@ static obligationst property_obligations_rec(
 
     if(next < no_timeframes)
     {
-      return property_obligations_rec(phi, solver, next, no_timeframes, ns);
+      return property_obligations_rec(phi, next, no_timeframes, ns);
     }
     else
     {
@@ -386,7 +381,7 @@ static obligationst property_obligations_rec(
     // p U q ≡ Fq ∧ (p W q)
     exprt tmp = and_exprt{F_exprt{q}, weak_U_exprt{p, q}};
 
-    return property_obligations_rec(tmp, solver, current, no_timeframes, ns);
+    return property_obligations_rec(tmp, current, no_timeframes, ns);
   }
   else if(property_expr.id() == ID_weak_U)
   {
@@ -399,7 +394,7 @@ static obligationst property_obligations_rec(
       q,
       (current + 1) < no_timeframes ? and_exprt{p, X_exprt{property_expr}} : p};
 
-    return property_obligations_rec(tmp, solver, current, no_timeframes, ns);
+    return property_obligations_rec(tmp, current, no_timeframes, ns);
   }
   else if(property_expr.id() == ID_R)
   {
@@ -414,8 +409,7 @@ static obligationst property_obligations_rec(
                         ? and_exprt{q, or_exprt{p, X_exprt{property_expr}}}
                         : q;
 
-    return property_obligations_rec(
-      expansion, solver, current, no_timeframes, ns);
+    return property_obligations_rec(expansion, current, no_timeframes, ns);
   }
   else if(
     property_expr.id() == ID_sva_until_with ||
@@ -432,7 +426,7 @@ static obligationst property_obligations_rec(
 
     tmp.op1() = X_exprt{tmp.op1()};
 
-    return property_obligations_rec(tmp, solver, current, no_timeframes, ns);
+    return property_obligations_rec(tmp, current, no_timeframes, ns);
   }
   else if(property_expr.id() == ID_and)
   {
@@ -442,8 +436,7 @@ static obligationst property_obligations_rec(
 
     for(auto &op : to_and_expr(property_expr).operands())
     {
-      obligations.add(
-        property_obligations_rec(op, solver, current, no_timeframes, ns));
+      obligations.add(property_obligations_rec(op, current, no_timeframes, ns));
     }
 
     return obligations;
@@ -459,7 +452,7 @@ static obligationst property_obligations_rec(
     for(auto &op : to_or_expr(property_expr).operands())
     {
       auto obligations =
-        property_obligations_rec(op, solver, current, no_timeframes, ns);
+        property_obligations_rec(op, current, no_timeframes, ns);
       auto conjunction = obligations.conjunction();
       t = std::max(t, conjunction.first);
       disjuncts.push_back(conjunction.second);
@@ -476,28 +469,26 @@ static obligationst property_obligations_rec(
     auto tmp = and_exprt{
       implies_exprt{equal_expr.lhs(), equal_expr.rhs()},
       implies_exprt{equal_expr.rhs(), equal_expr.lhs()}};
-    return property_obligations_rec(tmp, solver, current, no_timeframes, ns);
+    return property_obligations_rec(tmp, current, no_timeframes, ns);
   }
   else if(property_expr.id() == ID_implies)
   {
     // we rely on NNF
     auto &implies_expr = to_implies_expr(property_expr);
     auto tmp = or_exprt{not_exprt{implies_expr.lhs()}, implies_expr.rhs()};
-    return property_obligations_rec(tmp, solver, current, no_timeframes, ns);
+    return property_obligations_rec(tmp, current, no_timeframes, ns);
   }
   else if(property_expr.id() == ID_if)
   {
     // we rely on NNF
     auto &if_expr = to_if_expr(property_expr);
     auto cond =
-      instantiate_property(if_expr.cond(), current, no_timeframes, ns).second;
+      instantiate_property(if_expr.cond(), current, no_timeframes).second;
     auto obligations_true =
-      property_obligations_rec(
-        if_expr.true_case(), solver, current, no_timeframes, ns)
+      property_obligations_rec(if_expr.true_case(), current, no_timeframes, ns)
         .conjunction();
     auto obligations_false =
-      property_obligations_rec(
-        if_expr.false_case(), solver, current, no_timeframes, ns)
+      property_obligations_rec(if_expr.false_case(), current, no_timeframes, ns)
         .conjunction();
     return obligationst{
       std::max(obligations_true.first, obligations_false.first),
@@ -509,7 +500,7 @@ static obligationst property_obligations_rec(
   {
     // drop reduntant type casts
     return property_obligations_rec(
-      to_typecast_expr(property_expr).op(), solver, current, no_timeframes, ns);
+      to_typecast_expr(property_expr).op(), current, no_timeframes, ns);
   }
   else if(property_expr.id() == ID_not)
   {
@@ -521,35 +512,35 @@ static obligationst property_obligations_rec(
       // ¬(φ U ψ) ≡ (¬φ R ¬ψ)
       auto &U = to_U_expr(op);
       auto R = R_exprt{not_exprt{U.lhs()}, not_exprt{U.rhs()}};
-      return property_obligations_rec(R, solver, current, no_timeframes, ns);
+      return property_obligations_rec(R, current, no_timeframes, ns);
     }
     else if(op.id() == ID_R)
     {
       // ¬(φ R ψ) ≡ (¬φ U ¬ψ)
       auto &R = to_R_expr(op);
       auto U = U_exprt{not_exprt{R.lhs()}, not_exprt{R.rhs()}};
-      return property_obligations_rec(U, solver, current, no_timeframes, ns);
+      return property_obligations_rec(U, current, no_timeframes, ns);
     }
     else if(op.id() == ID_G)
     {
       // ¬G φ ≡ F ¬φ
       auto &G = to_G_expr(op);
       auto F = F_exprt{not_exprt{G.op()}};
-      return property_obligations_rec(F, solver, current, no_timeframes, ns);
+      return property_obligations_rec(F, current, no_timeframes, ns);
     }
     else if(op.id() == ID_F)
     {
       // ¬F φ ≡ G ¬φ
       auto &F = to_F_expr(op);
       auto G = G_exprt{not_exprt{F.op()}};
-      return property_obligations_rec(G, solver, current, no_timeframes, ns);
+      return property_obligations_rec(G, current, no_timeframes, ns);
     }
     else if(op.id() == ID_X)
     {
       // ¬X φ ≡ X ¬φ
       auto &X = to_X_expr(op);
       auto negX = X_exprt{not_exprt{X.op()}};
-      return property_obligations_rec(negX, solver, current, no_timeframes, ns);
+      return property_obligations_rec(negX, current, no_timeframes, ns);
     }
     else if(op.id() == ID_implies)
     {
@@ -557,8 +548,7 @@ static obligationst property_obligations_rec(
       auto &implies_expr = to_implies_expr(op);
       auto and_expr =
         and_exprt{implies_expr.lhs(), not_exprt{implies_expr.rhs()}};
-      return property_obligations_rec(
-        and_expr, solver, current, no_timeframes, ns);
+      return property_obligations_rec(and_expr, current, no_timeframes, ns);
     }
     else if(op.id() == ID_and)
     {
@@ -566,8 +556,7 @@ static obligationst property_obligations_rec(
       for(auto &op : operands)
         op = not_exprt{op};
       auto or_expr = or_exprt{std::move(operands)};
-      return property_obligations_rec(
-        or_expr, solver, current, no_timeframes, ns);
+      return property_obligations_rec(or_expr, current, no_timeframes, ns);
     }
     else if(op.id() == ID_or)
     {
@@ -575,22 +564,21 @@ static obligationst property_obligations_rec(
       for(auto &op : operands)
         op = not_exprt{op};
       auto and_expr = and_exprt{std::move(operands)};
-      return property_obligations_rec(
-        and_expr, solver, current, no_timeframes, ns);
+      return property_obligations_rec(and_expr, current, no_timeframes, ns);
     }
     else if(op.id() == ID_not)
     {
       return property_obligations_rec(
-        to_not_expr(op).op(), solver, current, no_timeframes, ns);
+        to_not_expr(op).op(), current, no_timeframes, ns);
     }
     else
       return obligationst{
-        instantiate_property(property_expr, current, no_timeframes, ns)};
+        instantiate_property(property_expr, current, no_timeframes)};
   }
   else
   {
     return obligationst{
-      instantiate_property(property_expr, current, no_timeframes, ns)};
+      instantiate_property(property_expr, current, no_timeframes)};
   }
 }
 
@@ -608,11 +596,10 @@ Function: property_obligations
 
 obligationst property_obligations(
   const exprt &property_expr,
-  decision_proceduret &solver,
   const mp_integer &no_timeframes,
   const namespacet &ns)
 {
-  return property_obligations_rec(property_expr, solver, 0, no_timeframes, ns);
+  return property_obligations_rec(property_expr, 0, no_timeframes, ns);
 }
 
 /*******************************************************************\
@@ -638,8 +625,7 @@ void property(
   // The first element of the pair is the length of the
   // counterexample, and the second is the condition that
   // must be valid for the property to hold.
-  auto obligations =
-    property_obligations(property_expr, solver, no_timeframes, ns);
+  auto obligations = property_obligations(property_expr, no_timeframes, ns);
 
   // Map obligations onto timeframes.
   prop_handles.resize(no_timeframes, true_exprt());
diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp
index b9c6581cd..eddc13cc7 100644
--- a/src/trans-word-level/sequence.cpp
+++ b/src/trans-word-level/sequence.cpp
@@ -17,8 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
   exprt expr,
   const mp_integer &t,
-  const mp_integer &no_timeframes,
-  const namespacet &ns)
+  const mp_integer &no_timeframes)
 {
   if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something
   {
@@ -40,7 +39,7 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
       }
       else
         return instantiate_sequence(
-          sva_cycle_delay_expr.op(), u, no_timeframes, ns);
+          sva_cycle_delay_expr.op(), u, no_timeframes);
     }
     else
     {
@@ -71,7 +70,7 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
       for(mp_integer u = lower; u <= upper; ++u)
       {
         auto sub_result =
-          instantiate_sequence(sva_cycle_delay_expr.op(), u, no_timeframes, ns);
+          instantiate_sequence(sva_cycle_delay_expr.op(), u, no_timeframes);
         for(auto &match_point : sub_result)
           match_points.push_back(match_point);
       }
@@ -89,7 +88,7 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
 
     // This is the product of the match points on the LHS and RHS
     const auto lhs_match_points =
-      instantiate_sequence(implication.lhs(), t, no_timeframes, ns);
+      instantiate_sequence(implication.lhs(), t, no_timeframes);
     for(auto &lhs_match_point : lhs_match_points)
     {
       // The RHS of the non-overlapped implication starts one timeframe later
@@ -105,7 +104,7 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
       }
 
       const auto rhs_match_points =
-        instantiate_sequence(implication.rhs(), t_rhs, no_timeframes, ns);
+        instantiate_sequence(implication.rhs(), t_rhs, no_timeframes);
 
       for(auto &rhs_match_point : rhs_match_points)
       {
@@ -157,8 +156,7 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
     exprt::operandst conjuncts;
 
     for(auto &op : expr.operands())
-      conjuncts.push_back(
-        instantiate_property(op, t, no_timeframes, ns).second);
+      conjuncts.push_back(instantiate_property(op, t, no_timeframes).second);
 
     exprt condition = conjunction(conjuncts);
     return {{t, condition}};
@@ -171,7 +169,7 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
     std::vector<std::pair<mp_integer, exprt>> result;
 
     for(auto &op : expr.operands())
-      for(auto &match_point : instantiate_sequence(op, t, no_timeframes, ns))
+      for(auto &match_point : instantiate_sequence(op, t, no_timeframes))
         result.push_back(match_point);
 
     return result;
@@ -179,6 +177,6 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
   else
   {
     // not a sequence, evaluate as state predicate
-    return {instantiate_property(expr, t, no_timeframes, ns)};
+    return {instantiate_property(expr, t, no_timeframes)};
   }
 }
diff --git a/src/trans-word-level/sequence.h b/src/trans-word-level/sequence.h
index b0df58cb7..c84770477 100644
--- a/src/trans-word-level/sequence.h
+++ b/src/trans-word-level/sequence.h
@@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 [[nodiscard]] std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
   exprt expr,
   const mp_integer &t,
-  const mp_integer &no_timeframes,
-  const namespacet &);
+  const mp_integer &no_timeframes);
 
 #endif // CPROVER_TRANS_WORD_LEVEL_SEQUENCE_H
diff --git a/src/trans-word-level/unwind.cpp b/src/trans-word-level/unwind.cpp
index cc8e1979b..441cb8865 100644
--- a/src/trans-word-level/unwind.cpp
+++ b/src/trans-word-level/unwind.cpp
@@ -6,12 +6,15 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <util/namespace.h>
-#include <util/find_symbols.h>
+#include "unwind.h"
+
 #include <util/expr_util.h>
+#include <util/find_symbols.h>
+#include <util/namespace.h>
+
+#include <solvers/decision_procedure.h>
 
 #include "instantiate_word_level.h"
-#include "unwind.h"
 
 /*******************************************************************\
 
@@ -44,8 +47,7 @@ void unwind(
 
   if(!op_invar.is_true())
     for(std::size_t c = 0; c < no_timeframes; c++)
-      decision_procedure.set_to_true(
-        instantiate(op_invar, c, no_timeframes, ns));
+      decision_procedure.set_to_true(instantiate(op_invar, c, no_timeframes));
 
   // initial state
 
@@ -54,8 +56,7 @@ void unwind(
     message.progress() << "Initial state" << messaget::eom;
 
     if(!op_init.is_true())
-      decision_procedure.set_to_true(
-        instantiate(op_init, 0, no_timeframes, ns));
+      decision_procedure.set_to_true(instantiate(op_init, 0, no_timeframes));
   }
 
   // transition relation
@@ -74,7 +75,6 @@ void unwind(
         message.progress() << "Transition " << t << "->" << t + 1
                            << messaget::eom;
 
-      decision_procedure.set_to_true(
-        instantiate(op_trans, t, no_timeframes, ns));
+      decision_procedure.set_to_true(instantiate(op_trans, t, no_timeframes));
     }
 }