diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
index 793f05b53..e1973eb9e 100644
--- a/src/ebmc/Makefile
+++ b/src/ebmc/Makefile
@@ -12,7 +12,6 @@ SRC = \
       diameter.cpp \
       diatest.cpp \
       dimacs_writer.cpp \
-      ebmc_base.cpp \
       ebmc_language.cpp \
       ebmc_language_file.cpp \
       ebmc_languages.cpp \
diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp
deleted file mode 100644
index 1dc8b596a..000000000
--- a/src/ebmc/ebmc_base.cpp
+++ /dev/null
@@ -1,188 +0,0 @@
-/*******************************************************************\
-
-Module: Base for Verification Modules
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#include "ebmc_base.h"
-
-#include <util/cmdline.h>
-#include <util/config.h>
-
-#include <trans-netlist/compute_ct.h>
-#include <trans-netlist/ldg.h>
-
-#include "ebmc_error.h"
-#include "ebmc_version.h"
-#include "netlist.h"
-
-#include <iostream>
-
-/*******************************************************************\
-
-Function: ebmc_baset::ebmc_baset
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-ebmc_baset::ebmc_baset(
-  const cmdlinet &_cmdline,
-  ui_message_handlert &_ui_message_handler)
-  : message(_ui_message_handler), cmdline(_cmdline)
-{
-}
-
-/*******************************************************************\
-
-Function: ebmc_baset::get_properties
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-int ebmc_baset::get_properties()
-{
-  properties = ebmc_propertiest::from_command_line(
-    cmdline, transition_system, message.get_message_handler());
-
-  return -1; // done
-}
-
-/*******************************************************************\
-
-Function: ebmc_baset::show_ldg
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void ebmc_baset::show_ldg(std::ostream &out)
-{
-  netlistt netlist;
-
-  if(make_netlist(netlist))
-    return;
-  
-  if(!netlist.transition.empty())
-    out << "WARNING: transition constraint found!" << '\n'
-        << '\n';
-  
-  ldgt ldg;
- 
-  ldg.compute(netlist);
-    
-  out << "Latch dependencies:" << '\n';
-
-  for(var_mapt::mapt::const_iterator
-      it=netlist.var_map.map.begin();
-      it!=netlist.var_map.map.end();
-      it++)
-  {
-    const var_mapt::vart &var=it->second;
-
-    for(std::size_t i=0; i<var.bits.size(); i++)
-    {
-      if(var.is_latch())
-      {
-        literalt::var_not v=var.bits[i].current.var_no();
-
-        out << "  " << it->first
-            << "[" << i << "] = " << v << ":";
-
-        const ldg_nodet &node=ldg[v];
-
-        for(ldg_nodet::edgest::const_iterator
-            i_it=node.in.begin();
-            i_it!=node.in.end();
-            i_it++)
-          out << " " << i_it->first;
-
-        out << '\n';
-      }
-    }
-  }
-}
-
-/*******************************************************************\
-
-Function: ebmc_baset::make_netlist
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-bool ebmc_baset::make_netlist(netlistt &netlist)
-{
-  // make net-list
-  message.status() << "Generating Netlist" << messaget::eom;
-
-  try
-  {
-    netlist = ::make_netlist(
-      transition_system, properties, message.get_message_handler());
-  }
-  
-  catch(const std::string &error_str)
-  {
-    message.error() << error_str << messaget::eom;
-    return true;
-  }
-
-  message.statistics() << "Latches: " << netlist.var_map.latches.size()
-                       << ", nodes: " << netlist.number_of_nodes()
-                       << messaget::eom;
-
-  return false;
-}
-
-/*******************************************************************\
-
-Function: ebmc_baset::do_compute_ct
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-int ebmc_baset::do_compute_ct()
-{
-  // make net-list
-  message.status() << "Making Netlist" << messaget::eom;
-
-  netlistt netlist;
-  if(make_netlist(netlist)) return 1;
-
-  message.status() << "Latches: " << netlist.var_map.latches.size()
-                   << ", nodes: " << netlist.number_of_nodes() << messaget::eom;
-
-  message.status() << "Making LDG" << messaget::eom;
-
-  ldgt ldg;
-  ldg.compute(netlist);
-
-  std::cout << "CT = " << compute_ct(ldg) << '\n';
-  
-  return 0;
-}
diff --git a/src/ebmc/ebmc_base.h b/src/ebmc/ebmc_base.h
deleted file mode 100644
index dafd7db8f..000000000
--- a/src/ebmc/ebmc_base.h
+++ /dev/null
@@ -1,61 +0,0 @@
-/*******************************************************************\
-
-Module: Base for Verification Modules
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#ifndef CPROVER_EBMC_EBMC_BASE_H
-#define CPROVER_EBMC_EBMC_BASE_H
-
-#include <util/cmdline.h>
-#include <util/message.h>
-#include <util/std_expr.h>
-#include <util/ui_message.h>
-
-#include <solvers/sat/cnf.h>
-#include <solvers/stack_decision_procedure.h>
-#include <trans-netlist/bmc_map.h>
-#include <trans-netlist/netlist.h>
-#include <trans-netlist/trans_trace.h>
-
-#include "ebmc_properties.h"
-#include "transition_system.h"
-
-#include <fstream>
-
-class ebmc_baset
-{
-public:
-  ebmc_baset(const cmdlinet &_cmdline,
-             ui_message_handlert &_ui_message_handler);
-  virtual ~ebmc_baset() { }
-
-  int get_properties();
-  void show_ldg(std::ostream &out);
-  bool make_netlist(netlistt &);
-
-  transition_systemt transition_system;
-
-  using propertyt = ebmc_propertiest::propertyt;
-  ebmc_propertiest properties;
-
-protected:
-  messaget message;
-  const cmdlinet &cmdline;
-
-  bool parse_property(const std::string &property);
-  bool get_model_properties();
-
-  bool parse();
-  bool parse(const std::string &filename);
-  bool typecheck();
-
-  std::size_t bound;
-
-public:
-  int do_compute_ct();
-};
-
-#endif
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index 478501507..d377a06ba 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -13,11 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/help_formatter.h>
 #include <util/string2int.h>
 
+#include <trans-netlist/compute_ct.h>
+#include <trans-netlist/ldg.h>
 #include <trans-netlist/smv_netlist.h>
 
 #include "build_transition_system.h"
 #include "diatest.h"
-#include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "ebmc_language.h"
 #include "ebmc_version.h"
@@ -270,10 +271,19 @@ int ebmc_parse_optionst::doit()
 
     if(cmdline.isset("show-ldg"))
     {
-      ebmc_baset ebmc_base(cmdline, ui_message_handler);
-      ebmc_base.transition_system = std::move(transition_system);
-      ebmc_base.properties = std::move(properties);
-      ebmc_base.show_ldg(std::cout);
+      auto netlist =
+        make_netlist(transition_system, properties, ui_message_handler);
+
+      if(!netlist.transition.empty())
+      {
+        messaget message(ui_message_handler);
+        message.warning() << "transition constraint found!" << messaget::eom;
+      }
+
+      ldgt ldg;
+      ldg.compute(netlist);
+      std::cout << "Latch dependencies:" << '\n';
+      ldg.output(netlist, std::cout);
       return 0;
     }
 
@@ -321,10 +331,21 @@ int ebmc_parse_optionst::doit()
 
     if(cmdline.isset("compute-ct"))
     {
-      ebmc_baset ebmc_base(cmdline, ui_message_handler);
-      ebmc_base.transition_system = std::move(transition_system);
-      ebmc_base.properties = std::move(properties);
-      return ebmc_base.do_compute_ct();
+      auto netlist =
+        make_netlist(transition_system, properties, ui_message_handler);
+
+      messaget message{ui_message_handler};
+
+      message.status() << "Latches: " << netlist.var_map.latches.size()
+                       << ", nodes: " << netlist.number_of_nodes()
+                       << messaget::eom;
+
+      message.status() << "Making LDG" << messaget::eom;
+
+      ldgt ldg;
+      ldg.compute(netlist);
+      std::cout << "CT = " << compute_ct(ldg) << '\n';
+      return 0;
     }
 
     auto checker_result = property_checker(
diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp
index d9e102805..978a11d60 100644
--- a/src/ebmc/random_traces.cpp
+++ b/src/ebmc/random_traces.cpp
@@ -20,9 +20,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <trans-word-level/trans_trace_word_level.h>
 #include <trans-word-level/unwind.h>
 
-#include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "output_file.h"
+#include "transition_system.h"
 #include "waveform.h"
 
 #include <algorithm>
diff --git a/src/ebmc/ranking_function.cpp b/src/ebmc/ranking_function.cpp
index c35cc948a..9a5602f5b 100644
--- a/src/ebmc/ranking_function.cpp
+++ b/src/ebmc/ranking_function.cpp
@@ -21,7 +21,6 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <trans-word-level/unwind.h>
 #include <verilog/sva_expr.h>
 
-#include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "property_checker.h"
diff --git a/src/ebmc/show_trans.cpp b/src/ebmc/show_trans.cpp
index 3e2c0aa94..a46076240 100644
--- a/src/ebmc/show_trans.cpp
+++ b/src/ebmc/show_trans.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <verilog/expr2verilog.h>
 
-#include "ebmc_base.h"
 #include "ebmc_version.h"
 #include "output_file.h"
 #include "output_verilog.h"
diff --git a/src/ic3/dnf_io.hh b/src/ic3/dnf_io.hh
index 25065f8e7..07e65a92e 100644
--- a/src/ic3/dnf_io.hh
+++ b/src/ic3/dnf_io.hh
@@ -10,6 +10,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #ifndef DNF_IO_HH
 #define DNF_IO_HH
 
+#include <cstdlib>
 #include <deque>
 #include <iosfwd>
 #include <map>
diff --git a/src/ic3/m4y_aiger_print.cc b/src/ic3/m4y_aiger_print.cc
index be2b2f660..7170b705f 100644
--- a/src/ic3/m4y_aiger_print.cc
+++ b/src/ic3/m4y_aiger_print.cc
@@ -6,21 +6,19 @@ Module: Printing circuit in text version of aiger format
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
-#include <queue>
-#include <set>
-#include <map>
+#include "ccircuit.hh"
+#include "dnf_io.hh"
+#include "m0ic3.hh"
+
 #include <algorithm>
 #include <iostream>
-
-#include <ebmc/ebmc_base.h>
+#include <map>
+#include <queue>
+#include <set>
 
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 
-#include "dnf_io.hh"
-#include "ccircuit.hh"
-#include "m0ic3.hh"
-
 /*====================================
 
  P R I N T _ A I G E R _ F O R M A T
diff --git a/src/ic3/m5y_aiger_print.cc b/src/ic3/m5y_aiger_print.cc
index 1387f7cef..705c5cc74 100644
--- a/src/ic3/m5y_aiger_print.cc
+++ b/src/ic3/m5y_aiger_print.cc
@@ -6,21 +6,19 @@ Module: Printing circuit in text version of aiger format
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
-#include <queue>
-#include <set>
-#include <map>
+#include "ccircuit.hh"
+#include "dnf_io.hh"
+#include "m0ic3.hh"
+
 #include <algorithm>
 #include <iostream>
-
-#include <ebmc/ebmc_base.h>
+#include <map>
+#include <queue>
+#include <set>
 
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 
-#include "dnf_io.hh"
-#include "ccircuit.hh"
-#include "m0ic3.hh"
-
 /*===========================================
 
      P R I N T _ A I G E R _ C O N S T R S
diff --git a/src/trans-netlist/ldg.cpp b/src/trans-netlist/ldg.cpp
index 9b04599c4..2bcffa1ba 100644
--- a/src/trans-netlist/ldg.cpp
+++ b/src/trans-netlist/ldg.cpp
@@ -98,3 +98,30 @@ void ldgt::compute(
     }
   }
 }
+
+void ldgt::output(const netlistt &netlist, std::ostream &out) const
+{
+  for(auto var_it : netlist.var_map.sorted())
+  {
+    auto &var = var_it->second;
+
+    for(std::size_t i = 0; i < var.bits.size(); i++)
+    {
+      if(var.is_latch())
+      {
+        literalt::var_not v = var.bits[i].current.var_no();
+
+        out << "  " << var_it->first << "[" << i << "] = " << v << ":";
+
+        const ldg_nodet &node = (*this)[v];
+
+        for(ldg_nodet::edgest::const_iterator i_it = node.in.begin();
+            i_it != node.in.end();
+            i_it++)
+          out << " " << i_it->first;
+
+        out << '\n';
+      }
+    }
+  }
+}
diff --git a/src/trans-netlist/ldg.h b/src/trans-netlist/ldg.h
index 267a6f108..e6d38894e 100644
--- a/src/trans-netlist/ldg.h
+++ b/src/trans-netlist/ldg.h
@@ -9,12 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_TRANS_LDG_H
 #define CPROVER_TRANS_LDG_H
 
-#include <set>
-
 #include <util/graph.h>
 
 #include "netlist.h"
 
+#include <iosfwd>
+#include <set>
+
 struct ldg_nodet:public graph_nodet<>
 {
 public:
@@ -35,6 +36,8 @@ class ldgt:public grapht<ldg_nodet>
   // latches that are to be considered
   void compute(const netlistt &netlist,
                const latchest &localization);
+
+  void output(const netlistt &, std::ostream &) const;
 };
 
 #endif