projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3f7bd44) | patch
[proofs] Alethe: Fix Bug in Finalize (#7746)
authorLachnitt <lachnitt@stanford.edu>
Tue, 7 Dec 2021 20:25:03 +0000 (12:25 -0800)
committerGitHub <noreply@github.com>
Tue, 7 Dec 2021 20:25:03 +0000 (20:25 +0000)
commitd5275e10906dd18ea2e83ab1b51b91e59ab59477
tree598c53c08d8774599218bdd35fcb98eb79380e08tree
parent3f7bd4478ff43359f4de09294226abdc453a7c58commit | diff
[proofs] Alethe: Fix Bug in Finalize (#7746)

Assumptions in Alethe are printed as (or F1 ... Fn) but should be treated as if they are printed as (cl (or F1 ... Fn)). Thus, if in the post visit it is checked whether an additional or step is needed this has to be treated as a special case.
src/proof/alethe/alethe_post_processor.cpp diff | blob | history