From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 23 Jun 2022 13:44:41 +0000 (-0700)
Subject: Fix rewrite for `(to_int real.pi)` (#8907)
X-Git-Tag: cvc5-1.0.1~38
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ce382efe5b7f2c31d1a4d13d06c9d9e2de270290;p=cvc5.git

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.
---

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index cfd4498c1..c6ac28950 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -793,7 +793,7 @@ RewriteResponse ArithRewriter::rewriteExtIntegerOp(TNode t)
   }
   if (t[0].getKind() == kind::PI)
   {
-    Node ret = isPred ? nm->mkConst(false) : nm->mkConstReal(Rational(3));
+    Node ret = isPred ? nm->mkConst(false) : nm->mkConstInt(Rational(3));
     return returnRewrite(t, ret, Rewrite::INT_EXT_PI);
   }
   else if (t[0].getKind() == kind::TO_REAL)
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 30f1d7177..945f31ea8 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -68,6 +68,7 @@ set(regress_0_tests
   regress0/arith/issue8097-iid.smt2
   regress0/arith/issue8159-rewrite-intreal.smt2
   regress0/arith/issue8805-mixed-var-elim.smt2
+  regress0/arith/issue8905-pi-to-int.smt2
   regress0/arith/ite-lift.smt2
   regress0/arith/leq.01.smtv1.smt2
   regress0/arith/miplib.cvc.smt2
diff --git a/test/regress/cli/regress0/arith/issue8905-pi-to-int.smt2 b/test/regress/cli/regress0/arith/issue8905-pi-to-int.smt2
new file mode 100644
index 000000000..199a17bf6
--- /dev/null
+++ b/test/regress/cli/regress0/arith/issue8905-pi-to-int.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_ALL)
+(assert (= 3 (to_int real.pi)))
+(set-info :status sat)
+(check-sat)