projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1b55d83) | patch
Fix type of null terminator for ADD/MULT for LFSC (#8762)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 12 May 2022 21:04:56 +0000 (16:04 -0500)
committerGitHub <noreply@github.com>
Thu, 12 May 2022 21:04:56 +0000 (21:04 +0000)
commitc2ddbb00d94253906c1a2a9f3d2abd6a0286698a
tree710916e0909fe9d8801c6259245913d4a98ef9eatree
parent1b55d831e0952a9260997414b713e05002bf4526commit | diff
Fix type of null terminator for ADD/MULT for LFSC (#8762)

This fixes many LFSC proof failures that are occurring now because of using 1.0 instead 1 as null terminator for MULT, and 0.0 instead of 0 for ADD.
src/expr/nary_term_util.cpp diff | blob | history
src/expr/node_converter.cpp diff | blob | history