projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fa43b88) | patch
Fix rewrite for `(to_int real.pi)` (#8907)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 23 Jun 2022 13:44:41 +0000 (06:44 -0700)
committerGitHub <noreply@github.com>
Thu, 23 Jun 2022 13:44:41 +0000 (08:44 -0500)
commitce382efe5b7f2c31d1a4d13d06c9d9e2de270290
tree6ea71cecb03690f994f9d3e5e2bccd18865993dctree
parentfa43b8842bd9082401cbf85c8de213a8ae152603commit | diff
Fix rewrite for `(to_int real.pi)` (#8907)

Fixes #8905. (to_int real.pi) was returning a real constant instead of
an integer, making the type of the rewritten term wrong.
src/theory/arith/arith_rewriter.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/arith/issue8905-pi-to-int.smt2 [new file with mode: 0644] blob