projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f3a5261) | patch
Remove redundant assertion in int-blaster (#8639)
authoryoni206 <yoni206@users.noreply.github.com>
Wed, 20 Apr 2022 14:48:31 +0000 (17:48 +0300)
committerGitHub <noreply@github.com>
Wed, 20 Apr 2022 14:48:31 +0000 (09:48 -0500)
commitf68d074187bd78f11204ce0f4480c7116100af19
tree1c35f6f84e96557d7eb521b932ac2184679b48cctree
parentf3a5261af19230d40ddc360fa5220ee03ab8d7f5commit | diff
Remove redundant assertion in int-blaster (#8639)

When translating nodes with no children, the default case does not change the original node, and so we do not need to assume anything about the node. fixes cvc5/cvc5-projects#416 . The example from the issue is added as a unit test.
src/theory/bv/int_blaster.cpp diff | blob | history
test/unit/api/cpp/solver_black.cpp diff | blob | history