Skip to content

Remove support for CVC 3 and CVC 4 #8967

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
tautschnig merged 1 commit into from
Apr 25, 2026
Merged

Remove support for CVC 3 and CVC 4 #8967

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 0 additions & 6 deletions doc/man/cbmc.1
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -495,12 +495,6 @@ use Boolector
\fB\-\-cprover\-smt2\fR
use CPROVER SMT2 solver
.TP
\fB\-\-cvc3\fR
use CVC3
.TP
\fB\-\-cvc4\fR
use CVC4
.TP
\fB\-\-cvc5\fR
use CVC5
.TP
Expand Down
6 changes: 0 additions & 6 deletions doc/man/goto-synthesizer.1
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,12 +61,6 @@ use Boolector
\fB\-\-cprover\-smt2\fR
use CPROVER SMT2 solver
.TP
\fB\-\-cvc3\fR
use CVC3
.TP
\fB\-\-cvc4\fR
use CVC4
.TP
\fB\-\-cvc5\fR
use CVC5
.TP
Expand Down
6 changes: 0 additions & 6 deletions doc/man/jbmc.1
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -413,12 +413,6 @@ use Boolector
\fB\-\-cprover\-smt2\fR
use CPROVER SMT2 solver
.TP
\fB\-\-cvc3\fR
use CVC3
.TP
\fB\-\-cvc4\fR
use CVC4
.TP
\fB\-\-cvc5\fR
use CVC5
.TP
Expand Down
12 changes: 0 additions & 12 deletions src/goto-checker/solver_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,10 +149,6 @@ smt2_dect::solvert solver_factoryt::get_smt2_solver_type() const
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"))
s = smt2_dect::solvert::CVC3;
else if(options.get_bool_option("cvc4"))
s = smt2_dect::solvert::CVC4;
else if(options.get_bool_option("cvc5"))
s = smt2_dect::solvert::CVC5;
else if(options.get_bool_option("yices"))
Expand Down Expand Up @@ -663,12 +659,6 @@ static void parse_smt2_options(const cmdlinet &cmdline, optionst &options)
options.set_option("smt2", true);
}

if(cmdline.isset("cvc4"))
{
options.set_option("cvc4", true), solver_set = true;
options.set_option("smt2", true);
}

if(cmdline.isset("cvc5"))
{
options.set_option("cvc5", true), solver_set = true;
Expand Down Expand Up @@ -742,8 +732,6 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options)
"boolector",
"cprover-smt2",
"mathsat",
"cvc3",
"cvc4",
"cvc5",
"yices",
"z3",
Expand Down
5 changes: 1 addition & 4 deletions src/goto-checker/solver_factory.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,8 +103,7 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
"(smt1)" /* rejected, will eventually disappear */ \
"(smt2)" \
"(fpa)" \
"(cvc3)" \
"(cvc4)(cvc5)(bitwuzla)(boolector)(yices)(z3)" \
"(cvc5)(bitwuzla)(boolector)(yices)(z3)" \
"(mathsat)" \
"(cprover-smt2)" \
"(incremental-smt2-solver):" \
Expand Down Expand Up @@ -133,8 +132,6 @@ void parse_solver_options(const cmdlinet &cmdline, optionst &options);
" {y--bitwuzla} \t use Bitwuzla\n" \
" {y--boolector} \t use Boolector\n" \
" {y--cprover-smt2} \t use CPROVER SMT2 solver\n" \
" {y--cvc3} \t use CVC3\n" \
" {y--cvc4} \t use CVC4\n" \
" {y--cvc5} \t use CVC5\n" \
" {y--mathsat} \t use MathSAT\n" \
" {y--yices} \t use Yices\n" \
Expand Down
11 changes: 0 additions & 11 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,15 +101,6 @@ smt2_convt::smt2_convt(
emit_set_logic = false;
break;

case solvert::CVC3:
break;

case solvert::CVC4:
logic = "ALL";
use_array_of_bool = true;
use_as_const = true;
break;

case solvert::CVC5:
logic = "ALL";
use_FPA_theory = true;
Expand Down Expand Up @@ -178,8 +169,6 @@ void smt2_convt::write_header()
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::CVC5: out << "; Generated for CVC 5\n"; break;
case solvert::MATHSAT: out << "; Generated for MathSAT\n"; break;
case solvert::YICES: out << "; Generated for Yices\n"; break;
Expand Down
2 changes: 0 additions & 2 deletions src/solvers/smt2/smt2_conv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,8 +47,6 @@ class smt2_convt : public stack_decision_proceduret
BITWUZLA,
BOOLECTOR,
CPROVER_SMT2,
CVC3,
CVC4,
CVC5,
MATHSAT,
YICES,
Expand Down
19 changes: 0 additions & 19 deletions src/solvers/smt2/smt2_dec.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,6 @@ std::string smt2_dect::decision_procedure_text() const
solver==solvert::BITWUZLA?"Bitwuzla":
solver==solvert::BOOLECTOR?"Boolector":
solver==solvert::CPROVER_SMT2?"CPROVER SMT2":
solver==solvert::CVC3?"CVC3":
solver==solvert::CVC4?"CVC4":
solver==solvert::CVC5?"CVC5":
solver==solvert::MATHSAT?"MathSAT":
solver==solvert::YICES?"Yices":
Expand Down Expand Up @@ -89,23 +87,6 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption)
stdin_filename = temp_file_problem();
break;

case solvert::CVC3:
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 = {solver_binary_name("cvc4"), "-L", "smt2", temp_file_problem()};
break;

case solvert::CVC5:
argv = {
solver_binary_name("cvc5"), "--lang", "smtlib", temp_file_problem()};
Expand Down
Loading