From 87b767424582b08b7df6814e12c5d96e29227164 Mon Sep 17 00:00:00 2001 From: "Douglas B. Staple" Date: Fri, 5 Aug 2016 14:11:51 -0300 Subject: [PATCH] Removed complete() from handling of y.is_zero() in process_power --- src/tactic/arith/purify_arith_tactic.cpp | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 6affe2fa0..463e1a9e8 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -410,14 +410,12 @@ struct purify_arith_proc { expr * x = args[0]; expr * zero = u().mk_numeral(rational(0), is_int); expr * one = u().mk_numeral(rational(1), is_int); - if (y.is_zero() && complete()) { + if (y.is_zero()) { // (^ x 0) --> k | x != 0 implies k = 1, x = 0 implies k = 0^0 push_cnstr(OR(EQ(x, zero), EQ(k, one))); push_cnstr_pr(result_pr); - if (complete()) { - push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real()))); - push_cnstr_pr(result_pr); - } + push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real()))); + push_cnstr_pr(result_pr); } else if (!is_int) { SASSERT(!y.is_int());