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.")

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index f829068cdf28f91ef53ecc276e006ea780d4b22c..1d82ac15bc15febe43bc31a62d771695bb4a7045 100644 (file)
--- 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 bce73046f01a57f4f0d20ef2d9fc411ab8c371ae..67f4b8cda49eb2674f42b12017974ca7921e5dca 100644 (file)
--- 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)
   {