From ce382efe5b7f2c31d1a4d13d06c9d9e2de270290 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 23 Jun 2022 06:44:41 -0700 Subject: [PATCH] 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 | 2 +- test/regress/cli/CMakeLists.txt | 1 + test/regress/cli/regress0/arith/issue8905-pi-to-int.smt2 | 4 ++++ 3 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 test/regress/cli/regress0/arith/issue8905-pi-to-int.smt2 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) -- 2.30.2