diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 3 | ||||
| -rw-r--r-- | src/theory/strings/proof_checker.cpp | 4 |
2 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 1a30f4449..8824859d4 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -201,6 +201,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, const std::vector<Node>& children, const std::vector<Node>& args) { + NodeManager * nm = NodeManager::currentNM(); // compute what was proven if (id == PfRule::ASSUME) { @@ -217,7 +218,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, // no antecedant return children[0]; } - Node ant = mkAnd(args); + Node ant = nm->mkAnd(args); // if the conclusion is false, its the negated antencedant only if (children[0].isConst() && !children[0].getConst<bool>()) { diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index ce2eb89ab..0b6cf6652 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -53,7 +53,7 @@ void StringProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::STRING_CODE_INJ, this); pc->registerChecker(PfRule::STRING_SEQ_UNIT_INJ, this); // trusted rules - pc->registerTrustedChecker(PfRule::STRING_TRUST, this, 1); + pc->registerTrustedChecker(PfRule::STRING_TRUST, this, 2); } Node StringProofRuleChecker::checkInternal(PfRule id, @@ -318,7 +318,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id, std::vector<Node> conj; ret = StringsPreprocess::reduce(t, conj, &skc); conj.push_back(t.eqNode(ret)); - ret = mkAnd(conj); + ret = nm->mkAnd(conj); } else if (id == PfRule::STRING_EAGER_REDUCTION) { |