projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e8eebe0) | patch
Fix debug failures in LFSC proofs due to curried arithmetic operators (#8763)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 13 May 2022 15:57:07 +0000 (10:57 -0500)
committerGitHub <noreply@github.com>
Fri, 13 May 2022 15:57:07 +0000 (15:57 +0000)
commitcbc1d2be703f91c2f8d94bcf853aac55e3709bcc
tree2691fd46160777b4584abd342c8f9e9e6f0235e3tree
parente8eebe0aaea199f8bd7ae8ef3348ca2985b20b59commit | diff
Fix debug failures in LFSC proofs due to curried arithmetic operators (#8763)

This ensures we use different variants of PLUS, MULT, NONLINEAR_MULT internally to avoid type checking failures in debug mode during LFSC printing.

Fixes regression failures in debug mode for LFSC.
src/proof/lfsc/lfsc_node_converter.cpp diff | blob | history
src/proof/lfsc/lfsc_post_processor.cpp diff | blob | history
src/proof/lfsc/lfsc_printer.cpp diff | blob | history