diff options
Diffstat (limited to 'src/theory/builtin')
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 3 |
1 files changed, 2 insertions, 1 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>()) { |