From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 11 Jan 2022 14:48:14 +0000 (-0600)
Subject: Guard use of unsat core mode pp-only (#7899)
X-Git-Tag: cvc5-1.0.0~568
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b3ec6979e39ea329e45c4158f51680fdd5858781;p=cvc5.git

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 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)
   {