diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp
index 70d29598e..6aeee5026 100644
--- a/src/ebmc/bdd_engine.cpp
+++ b/src/ebmc/bdd_engine.cpp
@@ -364,6 +364,10 @@ void bdd_enginet::compute_counterexample(
   propertyt &property,
   unsigned number_of_timeframes)
 {
+  // Supported by BMC engine?
+  if(!netlist_bmc_supports_property(property.normalized_expr))
+    return;
+
   message.status() << "Computing counterexample with " << number_of_timeframes
                    << " timeframe(s)" << messaget::eom;
 
@@ -372,16 +376,14 @@ void bdd_enginet::compute_counterexample(
   satcheckt solver{message.get_message_handler()};
   bmc_map.map_timeframes(netlist, number_of_timeframes, solver);
 
-  const namespacet ns(transition_system.symbol_table);
-
   ::unwind(netlist, bmc_map, message, solver);
+
+  // find the netlist property
+  auto netlist_property = netlist.properties.find(property.identifier);
+  CHECK_RETURN(netlist_property != netlist.properties.end());
+
   ::unwind_property(
-    property.normalized_expr,
-    property.timeframe_literals,
-    message.get_message_handler(),
-    solver,
-    bmc_map,
-    ns);
+    netlist_property->second, bmc_map, property.timeframe_literals);
 
   // we need the propertyt to fail in one of the timeframes
   bvt clause=property.timeframe_literals;
@@ -402,6 +404,8 @@ void bdd_enginet::compute_counterexample(
     throw "unexpected result from SAT solver";
   }
 
+  const namespacet ns(transition_system.symbol_table);
+
   property.witness_trace =
     compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns);
 }
diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp
index bddad5acd..8f7443162 100644
--- a/src/ebmc/ebmc_base.cpp
+++ b/src/ebmc/ebmc_base.cpp
@@ -208,13 +208,12 @@ int ebmc_baset::do_bit_level_bmc(cnft &solver, bool convert_only)
         continue;
       }
 
+      // look up the property in the netlist
+      auto netlist_property = netlist.properties.find(property.identifier);
+      CHECK_RETURN(netlist_property != netlist.properties.end());
+
       ::unwind_property(
-        property.normalized_expr,
-        property.timeframe_literals,
-        message.get_message_handler(),
-        solver,
-        bmc_map,
-        ns);
+        netlist_property->second, bmc_map, property.timeframe_literals);
 
       // freeze for incremental usage
       for(auto l : property.timeframe_literals)
diff --git a/src/ebmc/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp
index b2f191910..25ab95413 100644
--- a/src/ebmc/ebmc_properties.cpp
+++ b/src/ebmc/ebmc_properties.cpp
@@ -67,12 +67,8 @@ ebmc_propertiest ebmc_propertiest::from_transition_system(
 
       properties.properties.push_back(propertyt());
       properties.properties.back().number = properties.properties.size() - 1;
-
-      if(symbol.pretty_name.empty())
-        properties.properties.back().name = symbol.name;
-      else
-        properties.properties.back().name = symbol.pretty_name;
-
+      properties.properties.back().identifier = symbol.name;
+      properties.properties.back().name = symbol.display_name();
       properties.properties.back().original_expr = symbol.value;
       properties.properties.back().normalized_expr =
         normalize_property(symbol.value);
diff --git a/src/ebmc/ebmc_properties.h b/src/ebmc/ebmc_properties.h
index ae4b3bd17..debd77fe4 100644
--- a/src/ebmc/ebmc_properties.h
+++ b/src/ebmc/ebmc_properties.h
@@ -26,7 +26,7 @@ class ebmc_propertiest
   {
   public:
     std::size_t number = 0;
-    irep_idt name;
+    irep_idt identifier, name;
     source_locationt location;
     std::string expr_string;
     irep_idt mode;
diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp
index 967c64338..1f0446b2a 100644
--- a/src/ebmc/report_results.cpp
+++ b/src/ebmc/report_results.cpp
@@ -55,7 +55,8 @@ void report_results(
         continue;
 
       json_objectt json_property;
-      json_property["identifier"] = json_stringt(id2string(property.name));
+      json_property["identifier"] =
+        json_stringt(id2string(property.identifier));
       json_property["status"] = json_stringt(property.status_as_string());
 
       if(property.has_witness_trace())
@@ -77,7 +78,7 @@ void report_results(
         continue;
 
       xmlt xml_result("result");
-      xml_result.set_attribute("property", id2string(property.name));
+      xml_result.set_attribute("property", id2string(property.identifier));
       xml_result.set_attribute("status", property.status_as_string());
 
       if(property.has_witness_trace())
diff --git a/src/trans-netlist/instantiate_netlist.cpp b/src/trans-netlist/instantiate_netlist.cpp
index e438c334d..34c60a029 100644
--- a/src/trans-netlist/instantiate_netlist.cpp
+++ b/src/trans-netlist/instantiate_netlist.cpp
@@ -12,355 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr_util.h>
 #include <util/std_expr.h>
 
+#include <solvers/flattening/boolbv.h>
 #include <verilog/sva_expr.h>
 
 #include <cassert>
 #include <cstdlib>
 
-/*******************************************************************\
-
-   Class: instantiate_bmc_mapt
-
- Purpose:
-
-\*******************************************************************/
-
-class instantiate_bmc_mapt:public boolbvt
-{
-public:
-  instantiate_bmc_mapt(const namespacet &_ns, propt &solver,
-                       message_handlert &message_handler,
-                       const bmc_mapt &_bmc_map, unsigned _current,
-                       unsigned _next)
-      : boolbvt(_ns, solver, message_handler), bmc_map(_bmc_map),
-        current(_current), next(_next) {}
-
-  typedef boolbvt SUB;
-
-  // overloading
-  using boolbvt::get_literal;
-  
-  virtual literalt convert_bool(const exprt &expr);
-  virtual literalt get_literal(const std::string &symbol, const unsigned bit);
-  virtual bvt convert_bitvector(const exprt &expr);
-   
-protected:   
-  // disable smart variable allocation,
-  // we already have literals for all variables
-  virtual bool boolbv_set_equality_to_true(const equal_exprt &expr) { return true; }
-  virtual bool set_equality_to_true(const equal_exprt &expr) { return true; }
-  
-  const bmc_mapt &bmc_map;
-  unsigned current, next;
-};
-
-/*******************************************************************\
-
-Function: instantiate_constraint
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void instantiate_constraint(
-  propt &solver,
-  const bmc_mapt &bmc_map,
-  const exprt &expr,
-  unsigned current, unsigned next,
-  const namespacet &ns,
-  message_handlert &message_handler)
-{
-  instantiate_bmc_mapt i(ns, solver, message_handler, bmc_map, current, next);
-
-  try
-  {
-    i.set_to_true(expr);
-  }
-
-  catch(const char *err)
-  {
-    messaget(message_handler).error() << err << messaget::eom;
-    exit(1);
-  }
-
-  catch(const std::string &err)
-  {
-    messaget(message_handler).error() << err << messaget::eom;
-    exit(1);
-  }
-}
-
-/*******************************************************************\
-
-Function: instantiate_convert
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-literalt instantiate_convert(
-  propt &solver,
-  const bmc_mapt &bmc_map,
-  const exprt &expr,
-  unsigned current, unsigned next,
-  const namespacet &ns,
-  message_handlert &message_handler)
-{
-  instantiate_bmc_mapt i(ns, solver, message_handler, bmc_map, current, next);
-
-  try
-  {
-    return i.convert(expr);
-  }
-
-  catch(const char *err)
-  {
-    messaget(message_handler).error() << err << messaget::eom;
-    exit(1);
-  }
-
-  catch(const std::string &err)
-  {
-    messaget(message_handler).error() << err << messaget::eom;
-    exit(1);
-  }
-}
-
-/*******************************************************************\
-
-Function: instantiate_convert
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void instantiate_convert(
-  propt &solver,
-  const bmc_mapt &bmc_map,
-  const exprt &expr,
-  unsigned current, unsigned next,
-  const namespacet &ns,
-  message_handlert &message_handler,
-  bvt &bv)
-{
-  instantiate_bmc_mapt i(ns, solver, message_handler, bmc_map, current, next);
-
-  try
-  {
-    bv=i.convert_bitvector(expr);
-  }
-
-  catch(const char *err)
-  {
-    messaget(message_handler).error() << err << messaget::eom;
-    exit(1);
-  }
-
-  catch(const std::string &err)
-  {
-    messaget(message_handler).error() << err << messaget::eom;
-    exit(1);
-  }
-}
-
-/*******************************************************************\
-
-Function: instantiate_bmc_mapt::convert_bool
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-literalt instantiate_bmc_mapt::convert_bool(const exprt &expr)
-{
-  if(expr.id()==ID_symbol || expr.id()==ID_next_symbol)
-  {
-    bvt result=convert_bitvector(expr);
-
-    if(result.size()!=1)
-      throw "expected one-bit result";
-
-    return result[0];
-  }
-  else if(expr.id()==ID_sva_overlapped_implication)
-  {
-    // same as regular implication
-    auto &sva_overlapped_implication = to_sva_overlapped_implication_expr(expr);
-    return prop.limplies(
-      convert_bool(sva_overlapped_implication.lhs()),
-      convert_bool(sva_overlapped_implication.rhs()));
-  }
-  else if(expr.id()==ID_sva_non_overlapped_implication)
-  {
-    // right-hand side is shifted by one tick
-    auto &sva_non_overlapped_implication =
-      to_sva_non_overlapped_implication_expr(expr);
-    literalt lhs = convert_bool(sva_non_overlapped_implication.lhs());
-    unsigned old_current = current;
-    unsigned old_next = next;
-    literalt rhs = convert_bool(sva_non_overlapped_implication.rhs());
-    // restore
-    current = old_current;
-    next = old_next;
-    return prop.limplies(lhs, rhs);
-  }
-  else if(expr.id()==ID_sva_cycle_delay) // ##[1:2] something
-  {
-    if(expr.operands().size()==3)
-    {
-      unsigned old_current=current;
-      unsigned old_next=next;
-      literalt result;
-
-      if(to_ternary_expr(expr).op1().is_nil())
-      {
-        mp_integer offset;
-        if(to_integer_non_constant(to_ternary_expr(expr).op0(), offset))
-          throw "failed to convert sva_cycle_delay offset";
-
-        current = old_current + offset.to_ulong();
-        next = old_next + offset.to_ulong();
-        result = convert_bool(to_ternary_expr(expr).op2());
-      }
-      else
-      {
-        mp_integer from, to;
-        if(
-          to_integer_non_constant(to_ternary_expr(expr).op0(), from) ||
-          to_integer_non_constant(to_ternary_expr(expr).op1(), to))
-        {
-          throw "failed to convert sva_cycle_delay offsets";
-        }
-
-        // this is an 'or'
-        bvt disjuncts;
-        
-        for(mp_integer offset=from; offset<to; ++offset)
-        {
-          current = old_current + offset.to_ulong();
-          next = old_next + offset.to_ulong();
-          disjuncts.push_back(convert_bool(to_ternary_expr(expr).op2()));
-        }
-        
-        result=prop.lor(disjuncts);
-      }
-
-      // restore      
-      current=old_current;
-      next=old_next;
-      return result;
-    }
-  }
-  else if(expr.id()==ID_sva_always)
-  {
-  }
-  else if(expr.id()==ID_sva_nexttime)
-  {
-  }
-  else if(expr.id()==ID_sva_s_nexttime)
-  {
-  }
-  else if(expr.id()==ID_sva_eventually)
-  {
-  }
-  else if(expr.id()==ID_sva_s_eventually)
-  {
-  }
-  else if(expr.id()==ID_sva_until)
-  {
-  }
-  else if(expr.id()==ID_sva_s_until)
-  {
-  }
-  else if(expr.id()==ID_sva_until_with)
-  {
-  }
-  else if(expr.id()==ID_sva_s_until_with)
-  {
-  }
-  else if(expr.id()==ID_sva_sequence_concatenation)
-  {
-    if(expr.operands().size()==2)
-      return prop.land(
-        convert_bool(to_binary_expr(expr).op0()),
-        convert_bool(to_binary_expr(expr).op1()));
-  }
-
-  return SUB::convert_bool(expr);
-}
-
-/*******************************************************************\
-
-Function: instantiate_bmc_mapt::convert_bitvector
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-bvt instantiate_bmc_mapt::convert_bitvector(const exprt &expr)
-{
-  if(expr.id()==ID_symbol || expr.id()==ID_next_symbol)
-  {
-    const irep_idt &identifier=expr.get(ID_identifier);
-
-    std::size_t width=boolbv_width(expr.type());
-
-    if(width!=0)
-    {
-      unsigned timeframe=(expr.id()==ID_symbol)?current:next;
-
-      bvt bv;
-      bv.resize(width);
-
-      for(std::size_t i=0; i<width; i++)
-        bv[i]=bmc_map.get(timeframe, identifier, i);
-
-      return bv;
-    }
-  }
-
-  return SUB::convert_bitvector(expr);
-}
-
-/*******************************************************************\
-
-Function: instantiate_bmc_mapt::get_literal
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-literalt instantiate_bmc_mapt::get_literal(
-  const std::string &symbol,
-  const unsigned bit)
-{
-  return bmc_map.get(current, symbol, bit);
-}
-
 /*******************************************************************\
 
    Class: instantiate_var_mapt
diff --git a/src/trans-netlist/instantiate_netlist.h b/src/trans-netlist/instantiate_netlist.h
index 41386806d..135277d0c 100644
--- a/src/trans-netlist/instantiate_netlist.h
+++ b/src/trans-netlist/instantiate_netlist.h
@@ -6,16 +6,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#ifndef CPROVER_BMC_INSTANTIATE_NETLIST_H
-#define CPROVER_BMC_INSTANTIATE_NETLIST_H
+#ifndef CPROVER_TRANS_NETLIST_INSTANTIATE_NETLIST_H
+#define CPROVER_TRANS_NETLIST_INSTANTIATE_NETLIST_H
 
 #include <util/expr.h>
-#include <util/namespace.h>
 #include <util/message.h>
+#include <util/namespace.h>
 
-#include <solvers/flattening/boolbv.h>
-
-#include "bmc_map.h"
+#include "var_map.h"
 
 // bit-level
 
@@ -41,29 +39,4 @@ void instantiate_convert(
   message_handlert &,
   bvt &bv);
 
-void instantiate_constraint(
-  propt &solver,
-  const bmc_mapt &bmc_map,
-  const exprt &expr,
-  unsigned current, unsigned next,
-  const namespacet &,
-  message_handlert &);
-
-literalt instantiate_convert(
-  propt &solver,
-  const bmc_mapt &bmc_map,
-  const exprt &expr,
-  unsigned current, unsigned next,
-  const namespacet &,
-  message_handlert &);
-  
-void instantiate_convert(
-  propt &solver,
-  const bmc_mapt &bmc_map,
-  const exprt &expr,
-  unsigned current, unsigned next,
-  const namespacet &,
-  message_handlert &,
-  bvt &bv);
-
-#endif
+#endif // CPROVER_TRANS_NETLIST_INSTANTIATE_NETLIST_H
diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp
index 5baacc4db..1d9bec73e 100644
--- a/src/trans-netlist/trans_to_netlist.cpp
+++ b/src/trans-netlist/trans_to_netlist.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/ebmc_util.h>
+#include <util/mathematical_expr.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 
diff --git a/src/trans-netlist/unwind_netlist.cpp b/src/trans-netlist/unwind_netlist.cpp
index b50bdc771..e413eda3d 100644
--- a/src/trans-netlist/unwind_netlist.cpp
+++ b/src/trans-netlist/unwind_netlist.cpp
@@ -34,7 +34,7 @@ void unwind(
   messaget &message,
   cnft &solver,
   bool add_initial_state,
-  unsigned t)
+  std::size_t t)
 {
   bool first=(t==0);
   bool last=(t==bmc_map.timeframe_map.size()-1);
@@ -123,7 +123,7 @@ void unwind(
   cnft &solver,
   bool add_initial_state)
 {
-  for(unsigned t=0; t<bmc_map.timeframe_map.size(); t++)
+  for(std::size_t t = 0; t < bmc_map.timeframe_map.size(); t++)
     unwind(netlist, bmc_map, message, solver, add_initial_state, t);
 }
 
@@ -140,15 +140,16 @@ Function: unwind_property
 \*******************************************************************/
 
 void unwind_property(
+  const netlistt::propertyt &property,
   const bmc_mapt &bmc_map,
-  literalt property_node,
   bvt &prop_bv)
 {
+  PRECONDITION(std::holds_alternative<netlistt::Gpt>(property));
+  auto property_node = std::get<netlistt::Gpt>(property).p;
+
   prop_bv.resize(bmc_map.timeframe_map.size());
 
-  for(unsigned t=0;
-      t<bmc_map.timeframe_map.size();
-      t++)
+  for(std::size_t t = 0; t < bmc_map.timeframe_map.size(); t++)
   {
     literalt l=bmc_map.translate(t, property_node);
     prop_bv[t]=l;
@@ -157,51 +158,6 @@ void unwind_property(
 
 /*******************************************************************\
 
-Function: unwind_property
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void unwind_property(
-  const exprt &property_expr,
-  bvt &prop_bv,
-  message_handlert &message_handler,
-  propt &solver,
-  const bmc_mapt &map,
-  const namespacet &ns)
-{
-  if(property_expr.is_true())
-  {
-    prop_bv.resize(map.get_no_timeframes(), const_literal(true));
-    return;
-  }
-
-  // We want AG p.
-  auto &p = [](const exprt &expr) -> const exprt & {
-    if(expr.id() == ID_AG)
-      return to_AG_expr(expr).op();
-    else if(expr.id() == ID_G)
-      return to_G_expr(expr).op();
-    else if(expr.id() == ID_sva_always)
-      return to_sva_always_expr(expr).op();
-    else
-      PRECONDITION(false);
-  }(property_expr);
-
-  for(unsigned c=0; c<map.get_no_timeframes(); c++)
-  {
-    literalt l=instantiate_convert(solver, map, p, c, c+1, ns, message_handler);
-    prop_bv.push_back(l);
-  }
-}
-
-/*******************************************************************\
-
 Function: netlist_bmc_supports_property
 
   Inputs:
diff --git a/src/trans-netlist/unwind_netlist.h b/src/trans-netlist/unwind_netlist.h
index 67e50f0ce..b72968fdf 100644
--- a/src/trans-netlist/unwind_netlist.h
+++ b/src/trans-netlist/unwind_netlist.h
@@ -10,12 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_TRANS_UNWIND_NETLIST_GRAPH_H
 
 #include <util/message.h>
-#include <util/namespace.h>
 
 #include <solvers/sat/cnf.h>
 
-#include "netlist.h"
 #include "bmc_map.h"
+#include "netlist.h"
 
 void unwind(
   const netlistt &netlist,
@@ -31,24 +30,15 @@ void unwind(
   messaget &message,
   cnft &solver,
   bool add_initial_state,
-  unsigned timeframe);
-
-// unwind a property that has not yet been converted
-void unwind_property(
-  const exprt &property_expr,
-  bvt &prop_bv,
-  message_handlert &,
-  propt &solver,
-  const bmc_mapt &,
-  const namespacet &);
+  std::size_t timeframe);
 
 // Is the property supported?
-bool netlist_bmc_supports_property(const exprt &);
+bool netlist_bmc_supports_property(const class exprt &);
 
-// unwind a property that is given as netlist node
+// unwind a netlist property
 void unwind_property(
+  const netlistt::propertyt &,
   const bmc_mapt &,
-  literalt property_node,
   bvt &prop_bv);
 
 #endif