From b3ec6979e39ea329e45c4158f51680fdd5858781 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 11 Jan 2022 08:48:14 -0600 Subject: [PATCH] Guard use of unsat core mode pp-only (#7899) Fixes cvc5/cvc5-projects#366. Now gives (error "Error in option parsing: Unsat core mode pp-only is for internal use only.") --- src/options/smt_options.toml | 1 - src/smt/set_defaults.cpp | 6 ++++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index f829068cd..1d82ac15b 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -173,7 +173,6 @@ name = "SMT Layer" help = "Produce unsat cores using solving under assumptions and preprocessing proofs." [[option.mode.PP_ONLY]] name = "pp-only" - help = "Not producing unsat cores, but tracking proofs of preprocessing (internal only)." [[option]] name = "minimalUnsatCores" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index bce73046f..67f4b8cda 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -62,6 +62,12 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) void SetDefaults::setDefaultsPre(Options& opts) { + // internal-only options + if (opts.smt.unsatCoresMode == options::UnsatCoresMode::PP_ONLY) + { + throw OptionException( + std::string("Unsat core mode pp-only is for internal use only.")); + } // implied options if (opts.smt.debugCheckModels) { -- 2.30.2