Deactivate smt1 option in JBMC

Replicates the same change already done in CBMC
NathanJPhillips · Jul 18, 2018 · ebae090 · ebae090
1 parent 04fcc5b
commit ebae090
Showing 1 changed file with 11 additions and 47 deletions.
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -268,22 +268,15 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
       cmdline.get_value("max-node-refinement"));
 
   // SMT Options
-  bool version_set=false;
 
   if(cmdline.isset("smt1"))
   {
-    options.set_option("smt1", true);
-    options.set_option("smt2", false);
-    version_set=true;
+    error() << "--smt1 is no longer supported" << eom;
+    exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
   if(cmdline.isset("smt2"))
-  {
-    // If both are given, smt2 takes precedence
-    options.set_option("smt1", false);
     options.set_option("smt2", true);
-    version_set=true;
-  }
 
   if(cmdline.isset("fpa"))
     options.set_option("fpa", true);
@@ -293,76 +286,47 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("boolector"))
   {
     options.set_option("boolector", true), solver_set=true;
-    if(!version_set)
-      options.set_option("smt2", true), version_set=true;
+    options.set_option("smt2", true);
   }
 
   if(cmdline.isset("mathsat"))
   {
     options.set_option("mathsat", true), solver_set=true;
-    if(!version_set)
-      options.set_option("smt2", true), version_set=true;
-  }
-
-  if(cmdline.isset("cvc3"))
-  {
-    options.set_option("cvc3", true), solver_set=true;
-    if(!version_set)
-      options.set_option("smt1", true), version_set=true;
+    options.set_option("smt2", true);
   }
 
   if(cmdline.isset("cvc4"))
   {
     options.set_option("cvc4", true), solver_set=true;
-    if(!version_set)
-      options.set_option("smt2", true), version_set=true;
+    options.set_option("smt2", true);
   }
 
   if(cmdline.isset("yices"))
   {
     options.set_option("yices", true), solver_set=true;
-    if(!version_set)
-      options.set_option("smt2", true), version_set=true;
+    options.set_option("smt2", true);
   }
 
   if(cmdline.isset("z3"))
   {
     options.set_option("z3", true), solver_set=true;
-    if(!version_set)
-      options.set_option("smt2", true), version_set=true;
-  }
-
-  if(cmdline.isset("opensmt"))
-  {
-    options.set_option("opensmt", true), solver_set=true;
-    if(!version_set)
-      options.set_option("smt1", true), version_set=true;
+    options.set_option("smt2", true);
   }
 
-  if(version_set && !solver_set)
+  if(cmdline.isset("smt2") && !solver_set)
   {
     if(cmdline.isset("outfile"))
     {
       // outfile and no solver should give standard compliant SMT-LIB
-      options.set_option("generic", true), solver_set=true;
+      options.set_option("generic", true);
     }
     else
     {
-      if(options.get_bool_option("smt1"))
-      {
-        options.set_option("boolector", true), solver_set=true;
-      }
-      else
-      {
-        INVARIANT(options.get_bool_option("smt2"), "smt2 set");
-        options.set_option("z3", true), solver_set=true;
-      }
+      // the default smt2 solver
+      options.set_option("z3", true);
     }
   }
 
-  // Either have solver and standard version set, or neither.
-  INVARIANT(version_set==solver_set, "solver and version set");
-
   if(cmdline.isset("beautify"))
     options.set_option("beautify", true);