From b8a228191a66ebef5307dc71cd69a1503d7b6b75 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Nov 2025 13:19:20 +0000 Subject: [PATCH] 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 --- doc/man/cbmc.1 | 4 + doc/man/goto-synthesizer.1 | 4 + doc/man/jbmc.1 | 4 + .../Failing_Assert1/external-smt-solver.desc | 8 ++ scripts/bash-autocomplete/cbmc.sh.template | 2 +- src/goto-checker/solver_factory.cpp | 9 +++ src/goto-checker/solver_factory.h | 3 + .../accelerate/scratch_program.h | 2 +- src/solvers/smt2/smt2_dec.cpp | 74 +++++++++++-------- src/solvers/smt2/smt2_dec.h | 3 + 10 files changed, 81 insertions(+), 32 deletions(-) create mode 100644 regression/cbmc/Failing_Assert1/external-smt-solver.desc diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index edf0502fd85..0e454caf4c1 100644 --- a/doc/man/cbmc.1 +++ b/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 diff --git a/doc/man/goto-synthesizer.1 b/doc/man/goto-synthesizer.1 index 036586a9de6..1b2b44ed343 100644 --- a/doc/man/goto-synthesizer.1 +++ b/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 diff --git a/doc/man/jbmc.1 b/doc/man/jbmc.1 index 24ca6ceccb0..05f70b7805b 100644 --- a/doc/man/jbmc.1 +++ b/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 diff --git a/regression/cbmc/Failing_Assert1/external-smt-solver.desc b/regression/cbmc/Failing_Assert1/external-smt-solver.desc new file mode 100644 index 00000000000..022bb780bbf --- /dev/null +++ b/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 diff --git a/scripts/bash-autocomplete/cbmc.sh.template b/scripts/bash-autocomplete/cbmc.sh.template index 60e003543e7..58629250372 100644 --- a/scripts/bash-autocomplete/cbmc.sh.template +++ b/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 diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index a82d914d7e3..ac67cb87600 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/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")) diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h index 6359d67bd53..4c0541f634c 100644 --- a/src/goto-checker/solver_factory.h +++ b/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" \ diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h index 36c44ad6a97..cbac0fba67c 100644 --- a/src/goto-instrument/accelerate/scratch_program.h +++ b/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(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) { } diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index e467db8e5ba..7f516674dda 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -65,60 +65,72 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption) std::vector argv; std::string stdin_filename; + auto solver_binary_name = [this](const std::string &solver_name) + { + if(solver_binary_or_empty.empty()) + return solver_name; + else + return solver_binary_or_empty; + }; + switch(solver) { case solvert::BITWUZLA: - argv = {"bitwuzla", temp_file_problem()}; + argv = {solver_binary_name("bitwuzla"), temp_file_problem()}; break; case solvert::BOOLECTOR: - argv = {"boolector", "--smt2", temp_file_problem(), "-m"}; + argv = { + solver_binary_name("boolector"), "--smt2", temp_file_problem(), "-m"}; break; case solvert::CPROVER_SMT2: - argv = {"smt2_solver"}; + argv = {solver_binary_name("smt2_solver")}; stdin_filename = temp_file_problem(); break; case solvert::CVC3: - argv = {"cvc3", - "+model", - "-lang", - "smtlib", - "-output-lang", - "smtlib", - temp_file_problem()}; + argv = { + solver_binary_name("cvc3"), + "+model", + "-lang", + "smtlib", + "-output-lang", + "smtlib", + temp_file_problem()}; break; case solvert::CVC4: // The flags --bitblast=eager --bv-div-zero-const help but only // work for pure bit-vector formulas. - argv = {"cvc4", "-L", "smt2", temp_file_problem()}; + argv = {solver_binary_name("cvc4"), "-L", "smt2", temp_file_problem()}; break; case solvert::CVC5: - argv = {"cvc5", "--lang", "smtlib", temp_file_problem()}; + argv = { + solver_binary_name("cvc5"), "--lang", "smtlib", temp_file_problem()}; break; case solvert::MATHSAT: // The options below were recommended by Alberto Griggio // on 10 July 2013 - argv = {"mathsat", - "-input=smt2", - "-preprocessor.toplevel_propagation=true", - "-preprocessor.simplification=7", - "-dpll.branching_random_frequency=0.01", - "-dpll.branching_random_invalidate_phase_cache=true", - "-dpll.restart_strategy=3", - "-dpll.glucose_var_activity=true", - "-dpll.glucose_learnt_minimization=true", - "-theory.bv.eager=true", - "-theory.bv.bit_blast_mode=1", - "-theory.bv.delay_propagated_eqs=true", - "-theory.fp.mode=1", - "-theory.fp.bit_blast_mode=2", - "-theory.arr.mode=1"}; + argv = { + solver_binary_name("mathsat"), + "-input=smt2", + "-preprocessor.toplevel_propagation=true", + "-preprocessor.simplification=7", + "-dpll.branching_random_frequency=0.01", + "-dpll.branching_random_invalidate_phase_cache=true", + "-dpll.restart_strategy=3", + "-dpll.glucose_var_activity=true", + "-dpll.glucose_learnt_minimization=true", + "-theory.bv.eager=true", + "-theory.bv.bit_blast_mode=1", + "-theory.bv.delay_propagated_eqs=true", + "-theory.fp.mode=1", + "-theory.fp.bit_blast_mode=2", + "-theory.arr.mode=1"}; stdin_filename = temp_file_problem(); break; @@ -126,15 +138,17 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption) case solvert::YICES: // command = "yices -smt -e " // Calling convention for older versions // Convention for 2.2.1 - argv = {"yices-smt2", temp_file_problem()}; + argv = {solver_binary_name("yices-smt2"), temp_file_problem()}; break; case solvert::Z3: - argv = {"z3", "-smt2", temp_file_problem()}; + argv = {solver_binary_name("z3"), "-smt2", temp_file_problem()}; break; case solvert::GENERIC: - UNREACHABLE; + PRECONDITION(!solver_binary_or_empty.empty()); + argv = {solver_binary_or_empty, temp_file_problem()}; + break; } int res = diff --git a/src/solvers/smt2/smt2_dec.h b/src/solvers/smt2/smt2_dec.h index e362e6f0109..2b51118aee2 100644 --- a/src/solvers/smt2/smt2_dec.h +++ b/src/solvers/smt2/smt2_dec.h @@ -31,8 +31,10 @@ 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) { } @@ -40,6 +42,7 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt std::string decision_procedure_text() const override; protected: + std::string solver_binary_or_empty; message_handlert &message_handler; resultt dec_solve(const exprt &) override;