Option exception when incompatible with proofs (#8064)

This changes set defaults so that it doesn't silently disable proofs or unsat cores.

Fixes cvc5/cvc5-projects#440.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 5a7181f7bd53631d7f24feb17f82f76d2913ac87..e444ea275447efa931136c92b2faede544cd41d3 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -169,13 +169,9 @@ void SetDefaults::setDefaultsPre(Options& opts)
     std::stringstream reasonNoProofs;
     if (incompatibleWithProofs(opts, reasonNoProofs))
     {
-      opts.smt.unsatCores = false;
-      opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF;
-      notifyModifyOption(
-          "produceProofs and unsatCores", "false", reasonNoProofs.str());
-      opts.smt.produceProofs = false;
-      opts.smt.checkProofs = false;
-      opts.smt.proofMode = options::ProofMode::OFF;
+      std::stringstream ss;
+      ss << reasonNoProofs.str() << " not supported with proofs or unsat cores";
+      throw OptionException(ss.str());
     }
   }
   if (d_isInternalSubsolver)

diff --git a/test/regress/regress0/quantifiers/lra-triv-gn.smt2 b/test/regress/regress0/quantifiers/lra-triv-gn.smt2
index 7cc9c2ea3c9eb83e28f914839dce4b0a067b1655..0d36d2037356adf8d68e5cbef91258702be7c1f6 100644 (file)
--- a/test/regress/regress0/quantifiers/lra-triv-gn.smt2
+++ b/test/regress/regress0/quantifiers/lra-triv-gn.smt2
@@ -1,5 +1,7 @@
-; COMMAND-LINE: --global-negate --no-check-unsat-cores
+; COMMAND-LINE: --global-negate
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
 (set-logic LRA)
 (set-info :status unsat)
 (assert (not (exists ((?X Real)) (>= (/ (- 13) 4) ?X))))

diff --git a/test/regress/regress1/issue3970-nl-ext-purify.smt2 b/test/regress/regress1/issue3970-nl-ext-purify.smt2
index c19884a632b4c13566ddce3558de0f0d2d9afce0..a48660bd8823e18b5205d82a559850c32e47a9e4 100644 (file)
--- a/test/regress/regress1/issue3970-nl-ext-purify.smt2
+++ b/test/regress/regress1/issue3970-nl-ext-purify.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: -q
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
 (set-logic QF_UFNRA)
 (set-option :nl-ext-purify true)
 (set-option :sygus-inference true)

diff --git a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2
index 9cb5cdac3f607605a9f90c8dcb74e86f3f43a68d..beafff29ba16fab89eba9e1601a75a1423f143f3 100644 (file)
--- a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2
+++ b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2
@@ -1,4 +1,5 @@
-; COMMAND-LINE:
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
 (set-logic HO_ALL)
 (set-option :ag-miniscope-quant true)
 (set-option :conjecture-gen true)

diff --git a/test/regress/regress1/sygus/issue3201.smt2 b/test/regress/regress1/sygus/issue3201.smt2
index f9df0e78203c2fbf17d47dd6472387b34ad7f09e..212fca782c45d911922ee57337e09b32a44476ae 100644 (file)
--- a/test/regress/regress1/sygus/issue3201.smt2
+++ b/test/regress/regress1/sygus/issue3201.smt2
@@ -1,5 +1,7 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-inference -q
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
 (set-logic ALL)
 (declare-fun v () Bool)
 (assert false)

diff --git a/test/regress/regress1/sygus/issue3247.smt2 b/test/regress/regress1/sygus/issue3247.smt2
index a02fbc5ce0e4efb6d1634e0007122f7b92855162..7e2f439ceada3c12e7219995ac61ebceff961265 100644 (file)
--- a/test/regress/regress1/sygus/issue3247.smt2
+++ b/test/regress/regress1/sygus/issue3247.smt2
@@ -1,5 +1,7 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-inference --strings-exp -q
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
 (set-logic ALL)
 (declare-fun a () String) 
 (declare-fun b () String) 

diff --git a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
index 711afb2d8bb6cca1447b33b19a74299ee2b68da3..48b4ab38c59d1ad5e714f66a4c18ce66c7f725ad 100644 (file)
--- a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
+++ b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
@@ -1,5 +1,7 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-inference --fmf-bound
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
 (set-logic HO_ALL)
 (declare-fun a () (_ BitVec 1))
 (assert (bvsgt (bvsmod a a) #b0))

diff --git a/test/regress/regress1/sygus/issue4009-qep.smt2 b/test/regress/regress1/sygus/issue4009-qep.smt2
index 71b9f20bd6937031310f8cd85d40367125a6c948..67007bac221307ea2026feacee18a589f8c6458c 100644 (file)
--- a/test/regress/regress1/sygus/issue4009-qep.smt2
+++ b/test/regress/regress1/sygus/issue4009-qep.smt2
@@ -1,5 +1,7 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-inference --sygus-qe-preproc -q
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
 (set-logic ALL)
 (declare-fun a () Real)
 (declare-fun b () Real)

diff --git a/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2
index cc0c329cde49111ec589560492e5734fff3f5514..426316be43a6787c41abad509613c3ac9ecac4aa 100644 (file)
--- a/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2
+++ b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2
@@ -1,3 +1,5 @@
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
 (set-logic ALL)
 (set-option :sygus-inference true)
 (set-option :sygus-simple-sym-break none)

diff --git a/test/regress/regress1/sygus/issue4083-var-shadow.smt2 b/test/regress/regress1/sygus/issue4083-var-shadow.smt2
index 91b77bfaaa473ea54498768d9aa016af26a4cdb7..0afc35e00467020cdc4cc5ff4613b9b03740167b 100644 (file)
--- a/test/regress/regress1/sygus/issue4083-var-shadow.smt2
+++ b/test/regress/regress1/sygus/issue4083-var-shadow.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: -q
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
 (set-logic ALL)
 (set-option :miniscope-quant true)
 (set-option :sygus-inference true)

diff --git a/test/regress/regress1/sygus/proj-issue185.smt2 b/test/regress/regress1/sygus/proj-issue185.smt2
index a3e4b8205dee00c17a653772818c7b36b9cc1ea2..141ab0ae00f8224b176223ecba791e3f14d6a47c 100644 (file)
--- a/test/regress/regress1/sygus/proj-issue185.smt2
+++ b/test/regress/regress1/sygus/proj-issue185.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: -q
 ; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: proof
 (set-logic ALL)
 (set-option :sygus-inference true)
 (set-info :status unsat)

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 124a68ead3037b4512a70c45bc78f3675cf201e6..c6a303c8fb3db6543e9400d00cc77b61509c553a 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -3003,6 +3003,19 @@ TEST_F(TestApiBlackSolver, proj_issue414)
   ASSERT_NO_THROW(slv.simplify(t54));
 }
 
+TEST_F(TestApiBlackSolver, proj_issue440)
+{
+  Solver slv;
+  slv.setLogic("QF_ALL");
+  slv.setOption("global-negate", "true");
+  slv.setOption("produce-unsat-cores", "true");
+  Sort s1 = slv.getBooleanSort();
+  Term t9 = slv.mkBoolean(true);
+  Term t109 = slv.mkTerm(Kind::NOT, {t9});
+  // should throw an option exception
+  ASSERT_THROW(slv.checkSatAssuming({t109}), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackSolver, proj_issue434)
 {
   Solver slv;