projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ee576b7) | patch
Fix spurious assertion failure caused by subtyping in LFSC proof postprocessor (...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 12 Apr 2022 22:35:05 +0000 (17:35 -0500)
committerGitHub <noreply@github.com>
Tue, 12 Apr 2022 22:35:05 +0000 (17:35 -0500)
commit714393e33a20dbd55f525fdc533968fb6c445cfa
tree5ed3ea1dc0a1a27a70037a477f483f6e6ada59b9tree
parentee576b76441b9ab423cfaaa744a25487d0cd829acommit | diff
Fix spurious assertion failure caused by subtyping in LFSC proof postprocessor (#8608)

Also removes an old case for parametric datatypes in getBaseType, which is incorrect since datatypes not longer use subtyping.

This avoids more assertion failures in debug mode for LFSC due to subtypes.
src/expr/type_node.cpp diff | blob | history
src/proof/lfsc/lfsc_node_converter.cpp diff | blob | history
src/proof/lfsc/lfsc_post_processor.cpp diff | blob | history