diff options
| -rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 738497ece..0928ebe53 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -54,6 +54,12 @@ bool AletheProofPostprocessCallback::update(Node res, switch (id) { + //================================================= Core rules + //======================== Assume and Scope + case PfRule::ASSUME: + { + return addAletheStep(AletheRule::ASSUME, res, res, children, {}, *cdp); + } default: { return addAletheStep(AletheRule::UNDEFINED, |