From 7102f90a3681cfca1df4052d4a1e2cbab37a81b9 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 28 Feb 2024 15:07:41 -0300 Subject: [PATCH] fix --- src/proof/alethe/alethe_post_processor.cpp | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 047900eb94e..ef9e405bd9d 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -2075,13 +2075,11 @@ bool AletheProofPostprocessCallback::maybeReplacePremiseProof(Node premise, // of EQ_RESOLVE. NodeManager* nm = NodeManager::currentNM(); Trace("alethe-proof") << "\n"; - CVC5_UNUSED AletheRule premiseProofRule = - getAletheRule(premisePf->getArguments()[0]); - CVC5_UNUSED AletheRule premiseChildProofRule = - getAletheRule(premisePf->getChildren()[0]->getArguments()[0]); + AletheRule premiseProofRule = getAletheRule(premisePf->getArguments()[0]); if ((premiseProofRule == AletheRule::CONTRACTION - || premiseProofRule == AletheRule::REORDERING) - && premiseChildProofRule == AletheRule::OR) + || premiseProofRule == AletheRule::REORDERING) + && getAletheRule(premisePf->getChildren()[0]->getArguments()[0]) + == AletheRule::OR) { // get great grand child std::shared_ptr premiseChildPf =