Ensure proofs are fully disabled when incompatible (#8092)

Was causing regression failures on proof-new when proofs + sygus are enabled. We now force proofs to be disabled.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 12cf15346d461b8f8f657dbcc20578b78d33a3b4..9f51dcc24b5017904bda30be02e11253088bda24 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -114,7 +114,7 @@ void SetDefaults::setDefaultsPre(Options& opts)
     {
       if (opts.smt.unsatCoresModeWasSetByUser)
       {
-        notifyModifyOption("unsatCoresMode", "full-proof", "enabling proofs");
+        notifyModifyOption("unsatCoresMode", "sat-proof", "enabling proofs");
       }
       opts.smt.unsatCores = true;
       opts.smt.unsatCoresMode = options::UnsatCoresMode::SAT_PROOF;
@@ -175,6 +175,7 @@ void SetDefaults::setDefaultsPre(Options& opts)
           "produceProofs and unsatCores", "false", reasonNoProofs.str());
       opts.smt.produceProofs = false;
       opts.smt.checkProofs = false;
+      opts.smt.proofMode = options::ProofMode::OFF;
     }
   }
   if (d_isInternalSubsolver)

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 82cca1083f3de258e847e0ac6f8eb16d7e0bc447..8879c43b820ad6a766c7a219e380f840db84db5e 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -938,6 +938,9 @@ Node DatatypesRewriter::sygusToBuiltinEval(Node n,
                                            const std::vector<Node>& args)
 {
   Assert(d_sygusEval != nullptr);
+  Assert (n.getType().isDatatype());
+  Assert (n.getType().getDType().isSygus());
+  Assert (n.getType().getDType().getSygusVarList().getNumChildren()==args.size());
   NodeManager* nm = NodeManager::currentNM();
   // constant arguments?
   bool constArgs = true;