Add --external-smt2-solver for custom solver path or custom options

Similar to `--external-sat-solver`: enable calling SMT2 solvers with a
non-default name or possibly wrapping a solver to pass additional
options.

Fixes: #8720

Author: tautschnig

doc/man/cbmc.1

@@ -516,6 +516,10 @@ use Z3
 \fB\-\-fpa\fR
 use theory of floating\-point arithmetic
 .TP
+\fB\-\-external\-smt2\-solver\fR \fIcmd\fR
+Use \fIcmd\fR to invoke the SMT2 solver. Combine with one of the solver choices
+for solver-specific constraints.
+.TP
 \fB\-\-refine\fR
 use refinement procedure (experimental)
 .TP

doc/man/goto-synthesizer.1

@@ -82,6 +82,10 @@ use Z3
 \fB\-\-fpa\fR
 use theory of floating\-point arithmetic
 .TP
+\fB\-\-external\-smt2\-solver\fR \fIcmd\fR
+Use \fIcmd\fR to invoke the SMT2 solver. Combine with one of the solver choices
+for solver-specific constraints.
+.TP
 \fB\-\-refine\fR
 use refinement procedure (experimental)
 .TP

doc/man/jbmc.1

@@ -434,6 +434,10 @@ use Z3
 \fB\-\-fpa\fR
 use theory of floating\-point arithmetic
 .TP
+\fB\-\-external\-smt2\-solver\fR \fIcmd\fR
+Use \fIcmd\fR to invoke the SMT2 solver. Combine with one of the solver choices
+for solver-specific constraints.
+.TP
 \fB\-\-refine\fR
 use refinement procedure (experimental)
 .TP

regression/cbmc/Failing_Assert1/external-smt-solver.desc

@@ -0,0 +1,8 @@
+CORE smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--z3 --external-smt2-solver z3 --trace
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

scripts/bash-autocomplete/cbmc.sh.template

@@ -40,7 +40,7 @@ _cbmc_autocomplete()
      _filedir -d
      return 0
      ;;
-   --external-sat-solver|--incremental-smt2-solver)
+   --external-sat-solver|--incremental-smt2-solver|--external-smt2-solver)
      #a switch that takes a file parameter of which we don't know an extension
      _filedir -f
      return 0

src/goto-checker/solver_factory.cpp

@@ -515,6 +515,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
       std::string("Generated by CBMC ") + CBMC_VERSION,
       "QF_AUFBV",
       solver,
+      options.get_option("external-smt2-solver"),
       message_handler);
 
     if(options.get_bool_option("fpa"))
@@ -672,6 +673,14 @@ static void parse_smt2_options(const cmdlinet &cmdline, optionst &options)
     options.set_option("smt2", true);
   }
 
+  if(cmdline.isset("external-smt2-solver"))
+  {
+    options.set_option(
+      "external-smt2-solver", cmdline.get_value("external-smt2-solver"));
+    solver_set = true;
+    options.set_option("smt2", true);
+  }
+
   if(cmdline.isset("smt2") && !solver_set)
   {
     if(cmdline.isset("outfile"))

src/goto-checker/solver_factory.h

@@ -104,6 +104,7 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   "(mathsat)"                                                                  \
   "(cprover-smt2)"                                                             \
   "(incremental-smt2-solver):"                                                 \
+  "(external-smt2-solver):"                                                    \
   "(sat-solver):"                                                              \
   "(external-sat-solver):"                                                     \
   "(no-sat-preprocessor)"                                                      \
@@ -135,6 +136,8 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
   " {y--yices} \t use Yices\n"                                                 \
   " {y--z3} \t use Z3\n"                                                       \
   " {y--fpa} \t use theory of floating-point arithmetic\n"                     \
+  " {y--external-smt2-solver} {ucmd} \t command to invoke SMT2 solver "        \
+  "(combine with one of the solver choices for solver-specific constraints)\n" \
   " {y--refine} \t use refinement procedure (experimental)\n"                  \
   " {y--refine-arrays} \t use refinement for arrays only\n"                    \
   " {y--refine-arithmetic} \t refinement of arithmetic expressions only\n"     \

src/goto-instrument/accelerate/scratch_program.h

@@ -74,7 +74,7 @@ class scratch_programt:public goto_programt
       symex(mh, symbol_table, equation, options, path_storage, guard_manager),
       satcheck(std::make_unique<satcheckt>(mh)),
       satchecker(ns, *satcheck, mh),
-      z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3, mh),
+      z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3, "", mh),
       checker(&z3) // checker(&satchecker)
   {
   }

src/solvers/smt2/smt2_dec.cpp

@@ -134,11 +134,17 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption)
     break;
 
   case solvert::GENERIC:
-    UNREACHABLE;
+    PRECONDITION(!solver_binary_or_empty.empty());
+    argv = {solver_binary_or_empty, temp_file_problem()};
+    break;
   }
 
-  int res =
-    run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr());
+  int res = run(
+    solver_binary_or_empty.empty() ? argv[0] : solver_binary_or_empty,
+    argv,
+    stdin_filename,
+    temp_file_stdout(),
+    temp_file_stderr());
 
   if(res<0)
   {

src/solvers/smt2/smt2_dec.h

@@ -31,15 +31,18 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt
     const std::string &_notes,
     const std::string &_logic,
     solvert _solver,
+    const std::string &_solver_binary_or_empty,
     message_handlert &_message_handler)
     : smt2_convt(_ns, _benchmark, _notes, _logic, _solver, stringstream),
+      solver_binary_or_empty(_solver_binary_or_empty),
       message_handler(_message_handler)
   {
   }
 
   std::string decision_procedure_text() const override;
 
 protected:
+  std::string solver_binary_or_empty;
   message_handlert &message_handler;
   resultt dec_solve(const exprt &) override;