fix rewriting of power

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Nov 9, 2020 · f78980c · f78980c
1 parent 7d205f1
commit f78980c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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;
     }