remove OpenSMT

Author: Daniel Kroening

src/cbmc/cbmc_solvers.cpp

@@ -47,8 +47,6 @@ smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
     s=smt2_dect::solvert::CVC3;
   else if(options.get_bool_option("cvc4"))
     s=smt2_dect::solvert::CVC4;
-  else if(options.get_bool_option("opensmt"))
-    s=smt2_dect::solvert::OPENSMT;
   else if(options.get_bool_option("yices"))
     s=smt2_dect::solvert::YICES;
   else if(options.get_bool_option("z3"))

src/solvers/smt2/smt2_conv.cpp

@@ -78,7 +78,6 @@ void smt2_convt::write_header()
   case solvert::CVC3: out << "; Generated for CVC 3\n"; break;
   case solvert::CVC4: out << "; Generated for CVC 4\n"; break;
   case solvert::MATHSAT: out << "; Generated for MathSAT\n"; break;
-  case solvert::OPENSMT: out << "; Generated for OPENSMT\n"; break;
   case solvert::YICES: out << "; Generated for Yices\n"; break;
   case solvert::Z3: out << "; Generated for Z3\n"; break;
   }

src/solvers/smt2/smt2_conv.h

@@ -35,7 +35,6 @@ class smt2_convt:public prop_convt
     CVC3,
     CVC4,
     MATHSAT,
-    OPENSMT,
     YICES,
     Z3
   };
@@ -82,9 +81,6 @@ class smt2_convt:public prop_convt
     case solvert::MATHSAT:
       break;
 
-    case solvert::OPENSMT:
-      break;
-
     case solvert::YICES:
       break;
 

src/solvers/smt2/smt2_dec.cpp

@@ -37,7 +37,6 @@ std::string smt2_dect::decision_procedure_text() const
      solver==solvert::CVC3?"CVC3":
      solver==solvert::CVC4?"CVC4":
      solver==solvert::MATHSAT?"MathSAT":
-     solver==solvert::OPENSMT?"OpenSMT":
      solver==solvert::YICES?"Yices":
      solver==solvert::Z3?"Z3":
      "(unknown)");
@@ -126,14 +125,6 @@ decision_proceduret::resultt smt2_dect::dec_solve()
             + " > "+smt2_temp_file.temp_result_filename;
     break;
 
-  case solvert::OPENSMT:
-    command = "opensmt "
-            + smt2_temp_file.temp_out_filename
-            + " > "
-            + smt2_temp_file.temp_result_filename;
-    break;
-
-
   case solvert::YICES:
     //    command = "yices -smt -e "   // Calling convention for older versions
     command = "yices-smt2 "  //  Calling for 2.2.1