diff options
-rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 2 | ||||
-rw-r--r-- | src/proof/alethe/alethe_post_processor.h | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 97afbdab0..6312f3140 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -444,8 +444,8 @@ bool AletheProofPostprocessCallback::addAletheStep( } bool AletheProofPostprocessCallback::addAletheStepFromOr( - Node res, AletheRule rule, + Node res, const std::vector<Node>& children, const std::vector<Node>& args, CDProof& cdp) diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h index 4a7d8cf61..587190524 100644 --- a/src/proof/alethe/alethe_post_processor.h +++ b/src/proof/alethe/alethe_post_processor.h @@ -89,15 +89,15 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback * This method internally calls addAletheStep. The kind of the given Node has * to be OR. * - * @param res The expected result of the application in form (or F1 ... Fn), * @param rule The id of the Alethe rule, + * @param res The expected result of the application in form (or F1 ... Fn), * @param children The children of the application, * @param args The arguments of the application * @param cdp The proof to add to * @return True if the step could be added, or false if not. */ - bool addAletheStepFromOr(Node res, - AletheRule rule, + bool addAletheStepFromOr(AletheRule rule, + Node res, const std::vector<Node>& children, const std::vector<Node>& args, CDProof& cdp); |