projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2c8f7a7) | patch
Fix internal type issue for congruence over quantifiers in LFSC post-processor (...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 14 Apr 2022 23:25:09 +0000 (18:25 -0500)
committerGitHub <noreply@github.com>
Thu, 14 Apr 2022 23:25:09 +0000 (23:25 +0000)
commit910887748fef32cf57c0bad3b5eac2c44d6f48f8
tree41699392e1847d926397fd80e09dbae48c814806tree
parent2c8f7a72fbd01c06e717a02a34d610e39cc20042commit | diff
Fix internal type issue for congruence over quantifiers in LFSC post-processor (#8619)

Avoids debug assertions in LFSC proof conversion when doing congruence over closures.
src/proof/lfsc/lfsc_node_converter.cpp diff | blob | history
src/proof/lfsc/lfsc_post_processor.cpp diff | blob | history