From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 11 Feb 2022 21:36:55 +0000 (-0600)
Subject: Ensure proofs are fully disabled when incompatible (#8092)
X-Git-Tag: cvc5-1.0.0~425
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c16b7a2ba98296a82ccf84e015a7e07f8487908d;p=cvc5.git

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 12cf15346..9f51dcc24 100644
--- 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 82cca1083..8879c43b8 100644
--- 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;