From f78980c81c5092c8f8b67be8933b8350a91d07ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Nov 2020 20:57:36 -0800 Subject: [PATCH] fix rewriting of power Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 10d6c65d7..594ded1b3 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1254,7 +1254,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res TRACE("arith", tout << mk_pp(arg1, m()) << " " << mk_pp(arg2, m()) << "\n";); if (is_num_x && x.is_one()) { - result = m_util.mk_numeral(rational(0), false); + result = m_util.mk_numeral(x, false); return BR_DONE; }