diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/booleans/proof_checker.cpp | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 2d2155f44..d0461248c 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -157,10 +157,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, return Node::null(); } NodeManager* nm = NodeManager::currentNM(); - return disjuncts.empty() - ? nm->mkConst<bool>(false) - : disjuncts.size() == 1 ? disjuncts[0] - : nm->mkNode(kind::OR, disjuncts); + return nm->mkOr(disjuncts); } if (id == PfRule::REORDERING) { @@ -297,10 +294,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n"; } Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop; - return clauseNodes.empty() - ? nm->mkConst(false) - : clauseNodes.size() == 1 ? clauseNodes[0] - : nm->mkNode(kind::OR, clauseNodes); + return nm->mkOr(clauseNodes); } if (id == PfRule::MACRO_RESOLUTION_TRUST) { |