From ee0dbf34f0d1bbded0512aef5168ea8c92e30df0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 16 Dec 2015 00:49:06 +0200
Subject: [PATCH] add completion (introducing negative root function symbols)
 to address regression introduced when fixing unsound handling of negative
 roots

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/pdr/pdr_context.cpp              | 1 -
 src/tactic/arith/purify_arith_tactic.cpp | 8 ++++----
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index ded7c14c2..b3648f38d 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -1158,7 +1158,6 @@ namespace pdr {
         while (!todo.empty()) {
             model_node* n = todo.back();
             model* md = 0;
-            ast_manager& m = n->pt().get_manager();
             if (!n->get_model_ptr()) {
                 if (models.find(n->state(), md)) {
                     TRACE("pdr", tout << n->state() << "\n";);
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index 47f7a5576..a41c6939e 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -366,7 +366,7 @@ struct purify_arith_proc {
                     push_cnstr(EQ(x, u().mk_power(k, u().mk_numeral(n, false))));
                     push_cnstr_pr(result_pr);
                 }
-                else if (complete()) {
+                else {
                     SASSERT(n.is_even());
                     // (^ x (/ 1 n)) --> k  |  x >= 0 implies (x = k^n and k >= 0), x < 0 implies k = neg-root(x, n)   
                     // when n is even
@@ -379,9 +379,9 @@ struct purify_arith_proc {
                                   EQ(k, u().mk_neg_root(x, u().mk_numeral(n, false)))));
                     push_cnstr_pr(result_pr);
                 }
-                else {
-                    return BR_FAILED;
-                }
+//                else {
+//                    return BR_FAILED;
+//                }
             }
             else {
                 // root not supported for integers.