From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 21 May 2021 20:48:39 +0000 (-0500)
Subject: Minor simplification to boolean proof checker (#6590)
X-Git-Tag: cvc5-1.0.0~1709
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d99cc0f25aad013886a9648c93423c64fab9bdd4;p=cvc5.git

Minor simplification to boolean proof checker (#6590)
---

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)
   {