From e3c0fd8b1031de5e7d1a4d263452c4245e3fe32d Mon Sep 17 00:00:00 2001
From: Miodrag Milanovic <mmicko@gmail.com>
Date: Mon, 9 Jan 2023 16:14:01 +0100
Subject: qbfsat support for cvc5, fixes #3608

---
 passes/sat/qbfsat.cc | 6 ++++--
 passes/sat/qbfsat.h  | 4 +++-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index 4580f194e..42d3e188a 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -416,6 +416,8 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
 					opt.solver = opt.Solver::Yices;
 				else if (args[opt.argidx+1] == "cvc4")
 					opt.solver = opt.Solver::CVC4;
+				else if (args[opt.argidx+1] == "cvc5")
+					opt.solver = opt.Solver::CVC5;
 				else
 					log_cmd_error("Unknown solver \"%s\".\n", args[opt.argidx+1].c_str());
 				opt.argidx++;
@@ -542,8 +544,8 @@ struct QbfSatPass : public Pass {
 		log("        hope that the solver supports optimizing quantified bitvector problems.\n");
 		log("\n");
 		log("    -solver <solver>\n");
-		log("        Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n");
-		log("        (default: yices)\n");
+		log("        Use a particular solver. Choose one of: \"z3\", \"yices\", \"cvc4\"\n");
+		log("        and \"cvc5\". (default: yices)\n");
 		log("\n");
 		log("    -solver-option <name> <value>\n");
 		log("        Set the specified solver option in the SMT-LIBv2 problem file.\n");
diff --git a/passes/sat/qbfsat.h b/passes/sat/qbfsat.h
index c96c6f818..8fb6093bc 100644
--- a/passes/sat/qbfsat.h
+++ b/passes/sat/qbfsat.h
@@ -29,7 +29,7 @@ struct QbfSolveOptions {
 	bool specialize = false, specialize_from_file = false, write_solution = false, nocleanup = false;
 	bool dump_final_smt2 = false, assume_outputs = false, assume_neg = false, nooptimize = false;
 	bool nobisection = false, sat = false, unsat = false, show_smtbmc = false;
-	enum Solver{Z3, Yices, CVC4} solver = Yices;
+	enum Solver{Z3, Yices, CVC4, CVC5} solver = Yices;
 	enum OptimizationLevel{O0, O1, O2} oflag = O0;
 	dict<std::string, std::string> solver_options;
 	int timeout = 0;
@@ -45,6 +45,8 @@ struct QbfSolveOptions {
 			return "yices";
 		else if (solver == Solver::CVC4)
 			return "cvc4";
+		else if (solver == Solver::CVC5)
+			return "cvc5";
 
 		log_cmd_error("unknown solver specified.\n");
 		return "";
-- 
cgit v1.2.3