projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 988c7b9) | patch
[proofs] Alethe: Bug Fix in Cong Rule (#8391)
authorLachnitt <lachnitt@stanford.edu>
Fri, 25 Mar 2022 18:59:26 +0000 (11:59 -0700)
committerGitHub <noreply@github.com>
Fri, 25 Mar 2022 18:59:26 +0000 (18:59 +0000)
commit75d1a09f9d797cc3449e1a922e978d21e50f4b15
treecbf997e7ff0040f858640d97113c6b8044323cectree
parent988c7b9b5da35132669805ff5bf63d029db2651bcommit | diff
[proofs] Alethe: Bug Fix in Cong Rule (#8391)

cvc5 suffered a segfault in the CONG rule because the refl step, e.g. (= v0 v0), was added without the cl connector, e.g. (cl (= v0 v0))
src/proof/alethe/alethe_post_processor.cpp diff | blob | history