clean out old solvers

Author: Daniel Kroening

src/ebmc/ebmc_solvers.cpp

@@ -11,9 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/cmdline.h>
 
-#include <solvers/cvc/cvc_dec.h>
-#include <solvers/dplib/dplib_dec.h>
-#include <solvers/smt1/smt1_dec.h>
 #include <solvers/smt2/smt2_dec.h>
 #include <solvers/flattening/boolbv.h>
 #include <solvers/sat/dimacs_cnf.h>
@@ -72,57 +69,6 @@ int ebmc_baset::do_dimacs()
 
 /*******************************************************************\
 
-Function: ebmc_baset::do_smt1
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-int ebmc_baset::do_smt1()
-{
-  const namespacet ns(symbol_table);
-
-  if(cmdline.isset("outfile"))
-  {
-    const std::string filename=cmdline.get_value("outfile");
-    std::ofstream out(filename.c_str());
-  
-    if(!out)
-    {
-      std::cerr << "Failed to open `"
-                << filename
-                << "'" << '\n';
-      return 1;
-    }
-
-    smt1_convt smt1_conv(
-      ns,
-      "ebmc",
-      "Generated by EBMC " EBMC_VERSION,
-      "QF_AUFBV",
-      smt1_convt::solvert::Z3,
-      out);
-     
-    return do_bmc(smt1_conv, true);
-  }
-
-  smt1_convt smt1_conv(
-    ns,
-    "ebmc",
-    "Generated by EBMC " EBMC_VERSION,
-    "QF_AUFBV",
-    smt1_convt::solvert::Z3,
-    std::cout);
-   
-  return do_bmc(smt1_conv, true);
-}
-
-/*******************************************************************\
-
 Function: ebmc_baset::do_smt2
 
   Inputs:
@@ -292,14 +238,14 @@ int ebmc_baset::do_boolector()
 {
   const namespacet ns(symbol_table);
 
-  smt1_dect smt1_dec(
+  smt2_dect smt2_dec(
     ns,
     "ebmc",
     "Generated by EBMC " EBMC_VERSION,
     "QF_AUFBV",
-    smt1_dect::solvert::BOOLECTOR);
+    smt2_dect::solvert::BOOLECTOR);
 
-  return do_bmc(smt1_dec, false);
+  return do_bmc(smt2_dec, false);
 }
 
 /*******************************************************************\