projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 473ce2d) | patch
Rewrite (pow2 x) to (pow 2 x) when x is a constant (#7849)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 21 Dec 2021 14:49:35 +0000 (16:49 +0200)
committerGitHub <noreply@github.com>
Tue, 21 Dec 2021 14:49:35 +0000 (08:49 -0600)
commit8f514283c62415abbc6498758cc128682984afcc
treec8979d4b5950ae27112503d40a55ddb2210852c7tree
parent473ce2dbd6265f75c080086d523a9f6e598016d5commit | diff
Rewrite (pow2 x) to (pow 2 x) when x is a constant (#7849)

Fixes https://github.com/cvc5/cvc5-projects/issues/371.
Fixes https://github.com/cvc5/cvc5-projects/issues/339.
Fixes https://github.com/cvc5/cvc5-projects/issues/333.

Variants of the tests in the above issues are added to this PR. In them, we expect to get an exception because the constant is too big.
src/theory/arith/arith_rewriter.cpp diff | blob | history
test/unit/api/cpp/solver_black.cpp diff | blob | history