From c16b7a2ba98296a82ccf84e015a7e07f8487908d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Feb 2022 15:36:55 -0600 Subject: [PATCH] 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. --- src/smt/set_defaults.cpp | 3 ++- src/theory/datatypes/datatypes_rewriter.cpp | 3 +++ 2 files changed, 5 insertions(+), 1 deletion(-) 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& 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; -- 2.30.2