add support for CPROVER SMT2 solver

Author: Daniel Kroening

src/cbmc/cbmc_parse_options.cpp

@@ -327,6 +327,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("smt2", true);
   }
 
+  if(cmdline.isset("cprover-smt2"))
+  {
+    options.set_option("cprover-smt2", true), solver_set = true;
+    options.set_option("smt2", true);
+  }
+
   if(cmdline.isset("mathsat"))
   {
     options.set_option("mathsat", true), solver_set=true;
@@ -955,8 +961,9 @@ void cbmc_parse_optionst::help()
     " --localize-faults            localize faults (experimental)\n"
     " --smt2                       use default SMT2 solver (Z3)\n"
     " --boolector                  use Boolector\n"
-    " --mathsat                    use MathSAT\n"
+    " --cprover-smt2               use CPROVER SMT2 solver\n"
     " --cvc4                       use CVC4\n"
+    " --mathsat                    use MathSAT\n"
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"

src/cbmc/cbmc_parse_options.h

@@ -46,7 +46,8 @@ class optionst;
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
   "(xml-ui)(xml-interface)(json-ui)" \
-  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
+  "(smt1)(smt2)(fpa)" \
+  "(cprover-smt2)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
   "(no-sat-preprocessor)" \
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\

src/cbmc/cbmc_solvers.cpp

@@ -41,6 +41,8 @@ smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
 
   if(options.get_bool_option("boolector"))
     s=smt2_dect::solvert::BOOLECTOR;
+  else if(options.get_bool_option("cprover-smt2"))
+    s = smt2_dect::solvert::CPROVER_SMT2;
   else if(options.get_bool_option("mathsat"))
     s=smt2_dect::solvert::MATHSAT;
   else if(options.get_bool_option("cvc3"))

src/solvers/smt2/smt2_conv.cpp

@@ -72,6 +72,7 @@ void smt2_convt::write_header()
   {
   case solvert::GENERIC: break;
   case solvert::BOOLECTOR: out << "; Generated for Boolector\n"; break;
+  case solvert::CPROVER_SMT2: out << "; Generated for the CPROVER SMT2 solver\n"; break;
   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;

src/solvers/smt2/smt2_conv.h

@@ -36,6 +36,7 @@ class smt2_convt:public prop_convt
   {
     GENERIC,
     BOOLECTOR,
+    CPROVER_SMT2,
     CVC3,
     CVC4,
     MATHSAT,
@@ -76,6 +77,11 @@ class smt2_convt:public prop_convt
     case solvert::BOOLECTOR:
       break;
 
+    case solvert::CPROVER_SMT2:
+      use_array_of_bool = true;
+      emit_set_logic = false;
+      break;
+
     case solvert::CVC3:
       break;
 

src/solvers/smt2/smt2_dec.cpp

@@ -25,6 +25,7 @@ std::string smt2_dect::decision_procedure_text() const
     " using "+
     (solver==solvert::GENERIC?"Generic":
      solver==solvert::BOOLECTOR?"Boolector":
+     solver==solvert::CPROVER_SMT2?"CPROVER SMT2":
      solver==solvert::CVC3?"CVC3":
      solver==solvert::CVC4?"CVC4":
      solver==solvert::MATHSAT?"MathSAT":
@@ -56,6 +57,11 @@ decision_proceduret::resultt smt2_dect::dec_solve()
     argv = {"boolector", "--smt2", temp_file_problem(), "-m"};
     break;
 
+  case solvert::CPROVER_SMT2:
+    argv = {"smt2_solver"};
+    stdin_filename = temp_file_problem();
+    break;
+
   case solvert::CVC3:
     argv = {"cvc3",
             "+model",