diff --git a/src/common b/src/common
index e4f1ecdb35b..ef872268350 100644
--- a/src/common
+++ b/src/common
@@ -159,7 +159,7 @@ else
 endif
 
 # select default solver to be minisat2 if no other is specified
-ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT),)
+ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT),)
   MINISAT2 = ../../minisat-2.2.1
 endif
 
@@ -167,10 +167,6 @@ ifneq ($(IPASIR),)
   CP_CXXFLAGS += -DHAVE_IPASIR
 endif
 
-ifneq ($(PRECOSAT),)
-  CP_CXXFLAGS += -DHAVE_PRECOSAT
-endif
-
 ifneq ($(PICOSAT),)
   CP_CXXFLAGS += -DHAVE_PICOSAT
 endif
diff --git a/src/config.inc b/src/config.inc
index 93b44e39a50..5f2b7d9d4ec 100644
--- a/src/config.inc
+++ b/src/config.inc
@@ -16,7 +16,6 @@ endif
 #LIB_GLPK = -lglpk
 
 # SAT-solvers we have
-#PRECOSAT = ../../precosat-576-7e5e66f-120112
 #PICOSAT = ../../picosat-959
 #LINGELING = ../../lingeling-587f-4882048-110513
 #CHAFF = ../../zChaff
@@ -25,16 +24,11 @@ endif
 #MINISAT2 = ../../minisat-2.2.1
 #IPASIR = ../../ipasir
 #GLUCOSE = ../../glucose-syrup
-#SMVSAT =
 
 # Extra library for SAT solver. This should link to the archive file to be used
 # when linking against an IPASIR solver.
 LIBSOLVER =
 
-ifneq ($(PRECOSAT),)
-  CP_CXXFLAGS += -DSATCHECK_PRECOSAT
-endif
-
 ifneq ($(PICOSAT),)
   CP_CXXFLAGS += -DSATCHECK_PICOSAT
 endif
@@ -63,10 +57,6 @@ ifneq ($(GLUCOSE),)
   CP_CXXFLAGS += -DSATCHECK_GLUCOSE
 endif
 
-ifneq ($(SMVSAT),)
-  CP_CXXFLAGS += -DSATCHECK_SMVSAT
-endif
-
 # Signing identity for MacOS Gatekeeper
 
 OSX_IDENTITY="Developer ID Application: Daniel Kroening"
diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
index 5acd6652114..19aa7d29c55 100644
--- a/src/solvers/CMakeLists.txt
+++ b/src/solvers/CMakeLists.txt
@@ -18,9 +18,6 @@ set(minisat2_source
 set(glucose_source
     ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_glucose.cpp
 )
-set(smvsat_source
-    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_smvsat.cpp
-)
 set(squolem2_source
     ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_squolem.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_squolem_core.cpp
@@ -29,9 +26,6 @@ set(cudd_source
     ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_bdd_core.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_skizzo_core.cpp
 )
-set(precosat_source
-    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_precosat.cpp
-)
 set(picosat_source
     ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_picosat.cpp
 )
@@ -44,9 +38,6 @@ set(booleforce_source
 set(minibdd_source
     ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD/example.cpp
 )
-set(limmat_source
-    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_limmat.cpp
-)
 
 file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
@@ -54,15 +45,12 @@ list(REMOVE_ITEM sources
     ${minisat_source}
     ${minisat2_source}
     ${glucose_source}
-    ${smvsat_source}
     ${squolem2_source}
     ${cudd_source}
-    ${precosat_source}
     ${picosat_source}
     ${lingeling_source}
     ${booleforce_source}
     ${minibdd_source}
-    ${limmat_source}
 )
 
 add_library(solvers ${sources})
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 958373871d0..ab0f2cb2f7f 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -36,12 +36,6 @@ ifneq ($(GLUCOSE),)
   CP_CXXFLAGS += -DHAVE_GLUCOSE -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
 endif
 
-ifneq ($(SMVSAT),)
-  SMVSAT_SRC=sat/satcheck_smvsat.cpp
-  SMVSAT_INCLUDE=-I $(SMVSAT)/include
-  SMVSAT_LIB=$(SMVSAT)/lib/libsmvsat$(LIBEXT)
-endif
-
 ifneq ($(SQUOLEM2),)
   SQUOLEM2_SRC=qbf/qbf_squolem.cpp qbf/qbf_squolem_core.cpp
   SQUOLEM2_INCLUDE=-I $(SQUOLEM2)
@@ -56,13 +50,6 @@ ifneq ($(CUDD),)
            -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
 endif
 
-ifneq ($(PRECOSAT),)
-  PRECOSAT_SRC=sat/satcheck_precosat.cpp
-  PRECOSAT_INCLUDE=-I $(PRECOSAT)
-  PRECOSAT_LIB=$(PRECOSAT)/precosat$(OBJEXT)
-  CP_CXXFLAGS += -DHAVE_PRECOSAT
-endif
-
 ifneq ($(PICOSAT),)
   PICOSAT_SRC=sat/satcheck_picosat.cpp
   PICOSAT_INCLUDE=-I $(PICOSAT)
@@ -77,13 +64,6 @@ ifneq ($(LINGELING),)
   CP_CXXFLAGS += -DHAVE_LINGELING
 endif
 
-ifneq ($(LIMMAT),)
-  LIMMAT_SRC=sat/satcheck_limmat.cpp
-  LIMMAT_INCLUDE=-I $(LIMMAT)
-  LIMMAT_LIB=$(LIMMAT)/liblimmat$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_LIMMAT
-endif
-
 SRC = $(BOOLEFORCE_SRC) \
       $(CHAFF_SRC) \
       $(CUDD_SRC) \
@@ -93,10 +73,7 @@ SRC = $(BOOLEFORCE_SRC) \
       $(IPASIR_SRC) \
       $(MINISAT_SRC) \
       $(PICOSAT_SRC) \
-      $(PRECOSAT_SRC) \
-      $(SMVSAT_SRC) \
       $(SQUOLEM2_SRC) \
-      $(LIMMAT_SRC) \
       cvc/cvc_conv.cpp \
       cvc/cvc_dec.cpp \
       flattening/arrays.cpp \
@@ -199,7 +176,6 @@ SRC = $(BOOLEFORCE_SRC) \
       sat/cnf_clause_list.cpp \
       sat/dimacs_cnf.cpp \
       sat/pbs_dimacs_cnf.cpp \
-      sat/read_dimacs_cnf.cpp \
       sat/resolution_proof.cpp \
       sat/satcheck.cpp \
       smt1/smt1_conv.cpp \
@@ -214,8 +190,8 @@ SRC = $(BOOLEFORCE_SRC) \
 INCLUDES += -I .. \
   $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
   $(IPASIR_INCLUDE) \
-  $(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
-	$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
+  $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
+	$(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
 
 CLEANFILES = solvers$(LIBEXT) \
   smt2_solver$(EXEEXT) smt2/smt2_solver$(OBJEXT) smt2/smt2_solver$(DEPEXT)
@@ -231,8 +207,8 @@ endif
 endif
 
 SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
-        $(MINISAT2_LIB) $(SMVSAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
-	$(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
+        $(MINISAT2_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
+        $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
 
 ###############################################################################
 
diff --git a/src/solvers/sat/read_dimacs_cnf.cpp b/src/solvers/sat/read_dimacs_cnf.cpp
deleted file mode 100644
index 4228851fcdf..00000000000
--- a/src/solvers/sat/read_dimacs_cnf.cpp
+++ /dev/null
@@ -1,105 +0,0 @@
-/*******************************************************************\
-
-Module: Reading DIMACS CNF
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-/// \file
-/// Reading DIMACS CNF
-
-#include "read_dimacs_cnf.h"
-
-#include <istream>
-#include <cstdlib> // for abs()
-
-#include <util/string2int.h>
-
-// #define VERBOSE
-
-void read_dimacs_cnf(std::istream &in, cnft &dest)
-{
-  #define DELIMITERS "\t\n\v\f\r "
-  #define CHAR_DELIMITERS "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
-
-  bvt new_bv;
-  std::string line;
-
-  while(getline(in, line))
-  {
-    line += " ";
-
-    while(true)
-    {
-      if(line.empty())
-        break;
-
-      #ifdef VERBOSE
-      std::cout << "begin line " << line << '\n';
-      #endif
-      size_t pos = line.find_first_of(DELIMITERS, 0);
-      #ifdef VERBOSE
-      std::cout << "pos " << pos << '\n';
-      #endif
-      size_t pos_char = line.find_first_of(CHAR_DELIMITERS, 0);
-
-      if(pos!=std::string::npos)
-      {
-        std::string decision = line.substr(0, pos);
-        line.erase(0, pos+1);
-        #ifdef VERBOSE
-        std::cout << "i am here\n";
-        std::cout << decision << '\n';
-        std::cout << "line" << line << '\n';
-        #endif
-        if(!decision.compare(std::string("c")))
-        {
-          #ifdef VERBOSE
-          std::cout << "c \n";
-          #endif
-          break;
-        }
-
-        if(!decision.compare(std::string("p")))
-        {
-          #ifdef VERBOSE
-          std::cout << "p \n";
-          #endif
-          break;
-        }
-
-        if(pos_char == std::string::npos) // no char present in the clause
-        {
-          int parsed_lit = unsafe_string2int(decision);
-          #ifdef VERBOSE
-          std::cout << "parsed_lit " << parsed_lit << " \n";
-          #endif
-          if(parsed_lit == 0)
-          {
-            bvt no_dup=cnft::eliminate_duplicates(new_bv);
-            #ifdef VERBOSE
-            std::cout << "calling lcnf " << new_bv.size() << '\n';
-            #endif
-            dest.lcnf(no_dup);
-            new_bv.clear();
-            no_dup.clear();
-          }
-          else
-          {
-            unsigned var = abs(parsed_lit); // because of the const variable
-            literalt l;
-            bool sign = (parsed_lit > 0) ? false : true;
-            l.set(var, sign);
-            #ifdef VERBOSE
-            std::cout << "setting l to " << l.get() << '\n';
-            #endif
-            new_bv.push_back(l);
-            if(dest.no_variables() <= var)
-              dest.set_no_variables(var+1);
-          }
-        }
-      }
-    }
-  }
-}
diff --git a/src/solvers/sat/read_dimacs_cnf.h b/src/solvers/sat/read_dimacs_cnf.h
deleted file mode 100644
index 96bb752867a..00000000000
--- a/src/solvers/sat/read_dimacs_cnf.h
+++ /dev/null
@@ -1,19 +0,0 @@
-/*******************************************************************\
-
-Module: Reading DIMACS CNF
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-/// \file
-/// Reading DIMACS CNF
-
-#ifndef CPROVER_SOLVERS_SAT_READ_DIMACS_CNF_H
-#define CPROVER_SOLVERS_SAT_READ_DIMACS_CNF_H
-
-#include "cnf.h"
-
-void read_dimacs_cnf(std::istream &in, cnft &dest);
-
-#endif // CPROVER_SOLVERS_SAT_READ_DIMACS_CNF_H
diff --git a/src/solvers/sat/satcheck.h b/src/solvers/sat/satcheck.h
index cc20e33476a..6896be55da4 100644
--- a/src/solvers/sat/satcheck.h
+++ b/src/solvers/sat/satcheck.h
@@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
 // #define SATCHECK_MINISAT2
 // #define SATCHECK_GLUCOSE
 // #define SATCHECK_BOOLEFORCE
-// #define SATCHECK_PRECOSAT
 // #define SATCHECK_PICOSAT
 // #define SATCHECK_LINGELING
 
@@ -47,10 +46,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #define SATCHECK_BOOLEFORCE
 #endif
 
-#if defined(HAVE_PRECOSAT) && !defined(SATCHECK_PRECOSAT)
-#define SATCHECK_PRECOSAT
-#endif
-
 #if defined(HAVE_PICOSAT) && !defined(SATCHECK_PICOSAT)
 #define SATCHECK_PICOSAT
 #endif
@@ -94,13 +89,6 @@ typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert;
 typedef satcheck_ipasirt satcheckt;
 typedef satcheck_ipasirt satcheck_no_simplifiert;
 
-#elif defined SATCHECK_PRECOSAT
-
-#include "satcheck_precosat.h"
-
-typedef satcheck_precosatt satcheckt;
-typedef satcheck_precosatt satcheck_no_simplifiert;
-
 #elif defined SATCHECK_PICOSAT
 
 #include "satcheck_picosat.h"
diff --git a/src/solvers/sat/satcheck_limmat.cpp b/src/solvers/sat/satcheck_limmat.cpp
deleted file mode 100644
index 10fd310ff35..00000000000
--- a/src/solvers/sat/satcheck_limmat.cpp
+++ /dev/null
@@ -1,137 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#include "satcheck_limmat.h"
-
-#include <cassert>
-
-extern "C"
-{
-#include "limmat.h"
-}
-
-satcheck_limmatt::satcheck_limmatt()
-{
-  solver=new_Limmat(NULL);
-}
-
-satcheck_limmatt::~satcheck_limmatt()
-{
-  if(solver!=NULL)
-    delete_Limmat(solver);
-}
-
-tvt satcheck_limmatt::l_get(literalt a) const
-{
-  if(a.is_true())
-    return tvt(true);
-  else if(a.is_false())
-    return tvt(false);
-
-  tvt result;
-  unsigned v=a.var_no();
-
-  assert(v<assignment.size());
-
-  switch(assignment[v])
-  {
-    case 0: result=tvt(false); break;
-    case 1: result=tvt(true); break;
-    default: result=tvt(tvt::tv_enumt::TV_UNKNOWN); break;
-  }
-
-  if(a.sign())
-    result=!result;
-
-  return result;
-}
-
-const std::string satcheck_limmatt::solver_text()
-{
-  return std::string("Limmat version ")+version_Limmat();
-}
-
-void satcheck_limmatt::copy_cnf()
-{
-  for(clausest::iterator it=clauses.begin();
-      it!=clauses.end();
-      it++)
-      // it=clauses.erase(it))
-  {
-    int *clause=new int[it->size()+1];
-
-    for(unsigned j=0; j<it->size(); j++)
-      clause[j]=(*it)[j].dimacs();
-
-    // zero-terminated
-    clause[it->size()]=0;
-
-    add_Limmat(solver, clause);
-
-    delete clause;
-  }
-}
-
-propt::resultt satcheck_limmatt::prop_solve()
-{
-  copy_cnf();
-
-  {
-    std::string msg=
-      std::to_string(maxvar_Limmat(solver))+" variables, "+
-      std::to_string(clauses_Limmat(solver))+" clauses";
-    messaget::status() << msg << messaget::eom;
-  }
-
-  int status=sat_Limmat(solver, -1);
-
-  {
-    std::string msg;
-
-    switch(status)
-    {
-     case 0:
-      msg="SAT checker: instance is UNSATISFIABLE";
-      break;
-
-     case 1:
-      msg="SAT checker: instance is SATISFIABLE";
-      break;
-
-     default:
-      msg="SAT checker failed: unknown result";
-      break;
-    }
-
-    messaget::status() << msg << messaget::eom;
-  }
-
-  if(status==0)
-  {
-    assignment.clear();
-    return P_UNSATISFIABLE;
-  }
-
-  if(status==1)
-  {
-    assignment.resize(no_variables()+1, 2); // unknown is default
-
-    for(const int *a=assignment_Limmat(solver); *a!=0; a++)
-    {
-      int v=*a;
-      if(v<0)
-        v=-v;
-      assert((unsigned)v<assignment.size());
-      assignment[v]=(*a)>=0;
-    }
-
-    return P_SATISFIABLE;
-  }
-
-  return P_ERROR;
-}
diff --git a/src/solvers/sat/satcheck_limmat.h b/src/solvers/sat/satcheck_limmat.h
deleted file mode 100644
index 91e8e3d9df8..00000000000
--- a/src/solvers/sat/satcheck_limmat.h
+++ /dev/null
@@ -1,33 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-
-#ifndef CPROVER_SOLVERS_SAT_SATCHECK_LIMMAT_H
-#define CPROVER_SOLVERS_SAT_SATCHECK_LIMMAT_H
-
-#include <vector>
-#include "dimacs_cnf.h"
-
-class satcheck_limmatt:public dimacs_cnft
-{
- public:
-  satcheck_limmatt();
-  virtual ~satcheck_limmatt();
-
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
-
-  void copy_cnf();
-
- protected:
-  struct Limmat *solver;
-  std::vector<unsigned char> assignment;
-};
-
-#endif // CPROVER_SOLVERS_SAT_SATCHECK_LIMMAT_H
diff --git a/src/solvers/sat/satcheck_precosat.cpp b/src/solvers/sat/satcheck_precosat.cpp
deleted file mode 100644
index 6e9a2248c94..00000000000
--- a/src/solvers/sat/satcheck_precosat.cpp
+++ /dev/null
@@ -1,121 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
-
-\*******************************************************************/
-
-#include "satcheck_precosat.h"
-
-#include <cassert>
-
-#include <util/threeval.h>
-
-#include <precosat.hh>
-
-#ifndef HAVE_PRECOSAT
-#error "Expected HAVE_PRECOSAT"
-#endif
-
-#define precosat_lit(a) ((a).var_no()*2 + !(a).sign())
-
-tvt satcheck_precosatt::l_get(literalt a) const
-{
-  if(a.is_constant())
-    return tvt(a.sign());
-
-  tvt result;
-
-  if(a.var_no()>solver->getMaxVar())
-    return tvt(tvt::tv_enumt::TV_UNKNOWN);
-
-  const int val=solver->val(precosat_lit(a));
-  if(val>0)
-    result=tvt(true);
-  else if(val<0)
-    result=tvt(false);
-  else
-    return tvt(tvt::tv_enumt::TV_UNKNOWN);
-
-  return result;
-}
-
-const std::string satcheck_precosatt::solver_text()
-{
-  return "PrecoSAT";
-}
-
-void satcheck_precosatt::lcnf(const bvt &bv)
-{
-  bvt new_bv;
-
-  if(process_clause(bv, new_bv))
-    return;
-
-  forall_literals(it, new_bv)
-    solver->add(precosat_lit(*it));
-
-  solver->add(0);
-
-  clause_counter++;
-}
-
-propt::resultt satcheck_precosatt::prop_solve()
-{
-  assert(status!=ERROR);
-
-  // We start counting at 1, thus there is one variable fewer.
-  {
-    std::string msg=
-      std::to_string(no_variables()-1)+" variables, "+
-      std::to_string(solver->getAddedOrigClauses())+" clauses";
-    messaget::status() << msg << messaget::eom;
-  }
-
-  std::string msg;
-
-  const int res=solver->solve();
-  if(res==1)
-  {
-    msg="SAT checker: instance is SATISFIABLE";
-    messaget::status() << msg << messaget::eom;
-    status=SAT;
-    return P_SATISFIABLE;
-  }
-  else
-  {
-    assert(res==-1);
-    msg="SAT checker: instance is UNSATISFIABLE";
-    messaget::status() << msg << messaget::eom;
-  }
-
-  status=UNSAT;
-  return P_UNSATISFIABLE;
-}
-
-void satcheck_precosatt::set_assignment(literalt a, bool value)
-{
-  assert(false);
-}
-
-satcheck_precosatt::satcheck_precosatt() :
-  solver(new PrecoSat::Solver())
-{
-  solver->init();
-}
-
-satcheck_precosatt::~satcheck_precosatt()
-{
-  delete solver;
-}
-
-/*
-void satcheck_precosatt::set_assumptions(const bvt &bv)
-{
-  assumptions=bv;
-
-  forall_literals(it, assumptions)
-    assert(!it->is_constant());
-}
-*/
diff --git a/src/solvers/sat/satcheck_precosat.h b/src/solvers/sat/satcheck_precosat.h
deleted file mode 100644
index 78caad55d7d..00000000000
--- a/src/solvers/sat/satcheck_precosat.h
+++ /dev/null
@@ -1,44 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
-
-\*******************************************************************/
-
-
-#ifndef CPROVER_SOLVERS_SAT_SATCHECK_PRECOSAT_H
-#define CPROVER_SOLVERS_SAT_SATCHECK_PRECOSAT_H
-
-#include "cnf.h"
-
-namespace PrecoSat // NOLINT(readability/namespace)
-{
-class Solver; // NOLINT(readability/identifiers)
-}
-
-class satcheck_precosatt:public cnf_solvert
-{
-public:
-  satcheck_precosatt();
-  virtual ~satcheck_precosatt();
-
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
-
-  virtual void lcnf(const bvt &bv);
-  virtual void set_assignment(literalt a, bool value);
-
-  // PicoSAT has this, PrecoSAT doesn't
-  // virtual bool is_in_conflict(literalt a) const;
-  // virtual void set_assumptions(const bvt &_assumptions);
-  virtual bool has_set_assumptions() const { return false; }
-  virtual bool has_is_in_conflict() const { return false; }
-
-protected:
-  PrecoSat::Solver *solver;
-  // bvt assumptions;
-};
-
-#endif // CPROVER_SOLVERS_SAT_SATCHECK_PRECOSAT_H
diff --git a/src/solvers/sat/satcheck_smvsat.cpp b/src/solvers/sat/satcheck_smvsat.cpp
deleted file mode 100644
index 1018a4d96b1..00000000000
--- a/src/solvers/sat/satcheck_smvsat.cpp
+++ /dev/null
@@ -1,233 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#include "satcheck_smvsat.h"
-
-#include <cassert>
-#include <stack>
-
-#include <satsolvercore.h>
-#include <interpolator.h>
-
-satcheck_smvsatt::satcheck_smvsatt()
-{
-  satsolver=
-    sat_instance_new_type(SATSOLVERCORE1, no_variables(), true);
-
-  // now we can do l_const
-  init_const();
-}
-
-satcheck_smvsat_coret::satcheck_smvsat_coret()
-{
-}
-
-satcheck_smvsatt::~satcheck_smvsatt()
-{
-}
-
-tvt satcheck_smvsatt::l_get(literalt a) const
-{
-  assert(status==SAT);
-
-  if(a.is_true())
-    return tvt(true);
-  else if(a.is_false())
-    return tvt(false);
-
-  tvt result;
-  unsigned v=a.var_no();
-
-  switch(sat_instance_value(satsolver, v))
-  {
-    case 0: result=tvt(false); break;
-    case 1: result=tvt(true); break;
-    default: result=tvt(tvt::tv_enumt::TV_UNKNOWN); break;
-  }
-
-  if(a.sign())
-    result=!result;
-
-  return result;
-}
-
-const std::string satcheck_smvsatt::solver_text()
-{
-  return std::string("SMVSAT");
-}
-
-void satcheck_smvsatt::lcnf(const bvt &bv)
-{
-  bvt tmp;
-
-  if(process_clause(bv, tmp))
-    return;
-
-  int *lits=new int[tmp.size()+1];
-
-  for(unsigned i=0; i<tmp.size(); i++)
-    lits[i]=tmp[i].dimacs();
-
-  // zero-terminated
-  lits[tmp.size()]=0;
-
-  sat_instance_add_clause(satsolver, lits);
-
-  clause_counter++;
-
-  delete[] lits;
-}
-
-propt::resultt satcheck_smvsatt::prop_solve()
-{
-  int result=sat_instance_solve(satsolver);
-
-  {
-    std::string msg;
-
-    switch(result)
-    {
-    case 0:
-      msg="SAT checker: instance is UNSATISFIABLE";
-      break;
-
-    case 1:
-      msg="SAT checker: instance is SATISFIABLE";
-      break;
-
-    default:
-      msg="SAT checker failed: unknown result";
-      break;
-    }
-
-    messaget::status() << msg << messaget::eom;
-  }
-
-  if(result==0)
-  {
-    status=UNSAT;
-    return P_UNSATISFIABLE;
-  }
-
-  if(result==1)
-  {
-    status=SAT;
-    return P_SATISFIABLE;
-  }
-
-  status=ERROR;
-
-  return P_ERROR;
-}
-
-propt::resultt satcheck_smvsat_coret::prop_solve()
-{
-  propt::resultt result=satcheck_smvsatt::prop_solve();
-
-  if(result==P_UNSATISFIABLE)
-  {
-    // TODO
-  }
-
-  return result;
-}
-
-void satcheck_smvsat_interpolatort::lcnf(const bvt &bv)
-{
-  bvt tmp;
-
-  if(process_clause(bv, tmp))
-    return;
-
-  int *lits=new int[tmp.size()+1];
-
-  for(unsigned i=0; i<tmp.size(); i++)
-    lits[i]=tmp[i].dimacs();
-
-  // zero-terminated
-  lits[tmp.size()]=0;
-
-  unsigned clause_id=sat_instance_add_clause(satsolver, lits);
-
-  if(partition_numbers.size()<=clause_id)
-    partition_numbers.resize(clause_id+1, -1);
-
-  partition_numbers[clause_id]=partition_no;
-
-  delete[] lits;
-}
-
-void satcheck_smvsat_interpolatort::interpolate(exprt &dest)
-{
-  // crate instance
-
-  // NOLINTNEXTLINE(readability/identifiers)
-  struct interpolator *interpolator_satsolver=
-    new_interpolator(satsolver);
-
-  // set partition numbers
-
-  for(unsigned i=0; i<partition_numbers.size(); i++)
-  {
-    short p=partition_numbers[i];
-    if(p!=-1)
-      interpolator_satsolver->set_clause_partition(i, p);
-  }
-
-  int output=interpolator_satsolver->interpolate(0, 0);
-
-  build_aig(*interpolator_satsolver, output, dest);
-
-  delete interpolator_satsolver;
-}
-
-void satcheck_smvsat_interpolatort::build_aig(
-  // NOLINTNEXTLINE(readability/identifiers)
-  struct interpolator &interpolator_satsolver,
-  int output,
-  exprt &dest)
-{
-  std::stack<entryt> stack;
-
-  stack.push(entryt(output, &dest));
-
-  while(!stack.empty())
-  {
-    entryt x=stack.top();
-    stack.pop();
-
-    bool invert=x.g<0;
-    int n=invert?-x.g:x.g;
-
-    assert(n!=0);
-
-    exprt &e=*x.e;
-
-    if(n==INT_MAX)
-      e.make_true();
-    else if(n<=satsolver->num_variables())
-    { // a SAT variable
-      e.id(ID_symbol);
-      e.set(ID_identifier, n);
-    }
-    else
-    {
-      e.id(ID_and);
-      e.operands().resize(2);
-
-      unsigned g0=interpolator_satsolver.aig_arg(n, 0);
-      unsigned g1=interpolator_satsolver.aig_arg(n, 1);
-
-      stack.push(entryt(g0, &e.op0()));
-      stack.push(entryt(g1, &e.op1()));
-    }
-
-    if(invert)
-      e.make_not();
-  }
-}
diff --git a/src/solvers/sat/satcheck_smvsat.h b/src/solvers/sat/satcheck_smvsat.h
deleted file mode 100644
index c9d13c1d000..00000000000
--- a/src/solvers/sat/satcheck_smvsat.h
+++ /dev/null
@@ -1,90 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-
-#ifndef CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H
-#define CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H
-
-#include <vector>
-#include <set>
-
-#include <util/expr.h>
-
-#include "cnf.h"
-
-class satcheck_smvsatt:public cnf_solvert
-{
-public:
-  satcheck_smvsatt();
-  virtual ~satcheck_smvsatt();
-
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
-  virtual void lcnf(const bvt &bv);
-
-protected:
-  // NOLINTNEXTLINE(readability/identifiers)
-  struct sat_instance *satsolver;
-};
-
-class satcheck_smvsat_coret:public satcheck_smvsatt
-{
-public:
-  satcheck_smvsat_coret();
-
-  virtual resultt prop_solve();
-
-  bool is_in_core(literalt l) const
-  {
-    assert(l.var_no()<in_core.size());
-    return in_core[l.var_no()];
-  }
-
-protected:
-  std::vector<bool> in_core;
-};
-
-class satcheck_smvsat_interpolatort:public satcheck_smvsatt
-{
-public:
-  satcheck_smvsat_interpolatort():partition_no(0)
-  {
-  }
-
-  void set_partition_no(short p)
-  {
-    partition_no=p;
-  }
-
-  void interpolate(exprt &dest);
-
-protected:
-  virtual void lcnf(const bvt &bv);
-  short partition_no;
-
-  std::vector<short> partition_numbers;
-
-  void build_aig(
-    // NOLINTNEXTLINE(readability/identifiers)
-    struct interpolator &interpolator_satsolver,
-    int output,
-    exprt &dest);
-
-  struct entryt
-  {
-    int g;
-    exprt *e;
-
-    entryt(int _g, exprt *_e):g(_g), e(_e)
-    {
-    }
-  };
-};
-
-#endif // CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H