(proof-new) Generalize single step helper in eager proof generator (#5046)

This allows single step proofs to have premises, closed by a SCOPE. This will be useful for array lemmas.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index c390a4b25..81c3e7816 100644
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -63,15 +63,15 @@ void CombinationCareGraph::combineTheories()
     Debug("combineTheories")
         << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
 
-    Node split = equality.orNode(equality.notNode());
     TrustNode tsplit;
     if (isProofEnabled())
     {
       // make proof of splitting lemma
-      tsplit = d_cmbsPg->mkTrustNode(split, PfRule::SPLIT, {equality});
+      tsplit = d_cmbsPg->mkTrustNodeSplit(equality);
     }
     else
     {
+      Node split = equality.orNode(equality.notNode());
       tsplit = TrustNode::mkTrustLemma(split, nullptr);
     }
     sendLemma(tsplit, carePair.d_theory);