From 2ff5af7d42c90efdce367a0cb13ee6a6e5aae90c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 19 Nov 2016 10:06:16 -0800
Subject: [PATCH] fix bug incorrect clearing of goals during node creation.
 Issue #777

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/dl_context.cpp      | 16 +++++++++++-----
 src/muz/pdr/pdr_context.cpp      |  8 +++-----
 src/muz/pdr/pdr_dl_interface.cpp |  1 +
 3 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 08fc0b9d7..2ca74a73b 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -1001,14 +1001,20 @@ namespace datalog {
                 if (is_quantifier(body)) {
                     quantifier* q = to_quantifier(body);
                     expr* e = q->get_expr();
-                    VERIFY(m.is_implies(e, body, e2));
-                    fml = m.mk_quantifier(false, q->get_num_decls(),
-                                          q->get_decl_sorts(), q->get_decl_names(),
-                                          body);
+                    if (m.is_implies(e, body, e2)) {
+                        fml = m.mk_quantifier(false, q->get_num_decls(),
+                                              q->get_decl_sorts(), q->get_decl_names(),
+                                              body);
+                    }
+                    else {
+                        fml = body;
+                    }
                 }
                 else {
-                    VERIFY(m.is_implies(body, body, e2));
                     fml = body;
+                    if (m.is_implies(body, body, e2)) {
+                        fml = body;
+                    }
                 }
                 queries.push_back(fml);
             }
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 01a9a4416..676f820b2 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -895,14 +895,12 @@ namespace pdr {
 
 
     void model_node::dequeue(model_node*& root) {
-        TRACE("pdr", tout << this << " " << state() << "\n";);
-        root = 0;
+        TRACE("pdr", tout << this << " root: " << root << " " << state() << "\n";);
         if (!m_next && !m_prev) return;
         SASSERT(m_next);
         SASSERT(m_prev);
         SASSERT(children().empty());
         if (this == m_next) {
-            // SASSERT(root == this);
             root = 0;
         }
         else {
@@ -975,7 +973,7 @@ namespace pdr {
     }
 
     void model_search::enqueue_leaf(model_node* n) {
-        TRACE("pdr_verbose", tout << n << " " << n->state() << " goal: " << m_goal << "\n";);
+        TRACE("pdr_verbose", tout << "node: " << n << " " << n->state() << " goal: " << m_goal << "\n";);
         SASSERT(n->is_open());
         if (!m_goal) {
             m_goal = n;
@@ -1005,7 +1003,7 @@ namespace pdr {
         return m_cache[l];
     }
 
-    void model_search::erase_children(model_node& n, bool backtrack) {
+    void model_search::erase_children(model_node& n, bool backtrack) {        
         ptr_vector<model_node> todo, nodes;
         todo.append(n.children());
         remove_goal(n);
diff --git a/src/muz/pdr/pdr_dl_interface.cpp b/src/muz/pdr/pdr_dl_interface.cpp
index dfc15636c..761b730ce 100644
--- a/src/muz/pdr/pdr_dl_interface.cpp
+++ b/src/muz/pdr/pdr_dl_interface.cpp
@@ -148,6 +148,7 @@ lbool dl_interface::query(expr * query) {
     TRACE("pdr",
           tout << "rules:\n";
           m_ctx.display_rules(tout);
+          m_ctx.display_smt2(0, 0, tout);
           );
 
     IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););