diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 177b87820..3b7d5c056 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -622,14 +622,14 @@ namespace pdr {
             m_rule2transition.insert(&rule, fml.get());
             rules.push_back(&rule);
         }
-        m_rule2inst.insert(&rule,&var_reprs);
+        m_rule2inst.insert(&rule, &var_reprs);
         m_rule2vars.insert(&rule, aux_vars);
         TRACE("pdr", 
               tout << rule.get_decl()->get_name() << "\n";
               for (unsigned i = 0; i < var_reprs.size(); ++i) {
                   tout << mk_pp(var_reprs[i].get(), m) << " ";
               }
-              tout << "\n";);
+              if (!var_reprs.empty()) tout << "\n";);
     }
 
     bool pred_transformer::check_filled(app_ref_vector const& v) const {
@@ -742,9 +742,26 @@ namespace pdr {
         m_closed = true; 
     }
 
-    void model_node::reopen() {
+    void model_node::set_open() {
         SASSERT(m_closed);
         m_closed = false;
+        model_node* p = parent();
+        while (p && p->is_closed()) {
+            p->m_closed = false;
+            p = p->parent();
+        }
+    }
+
+    void model_node::check_pre_closed() {
+        for (unsigned i = 0; i < children().size(); ++i) {
+            if (children()[i]->is_open()) return;
+        }
+        set_pre_closed();
+        model_node* p = parent();
+        while (p && p->is_1closed()) {
+            p->set_pre_closed();
+            p = p->parent();
+        }
     }
 
     static bool is_ini(datalog::rule const& r) {
@@ -852,22 +869,66 @@ namespace pdr {
     }
 
 
+    void model_node::dequeue(model_node*& root) {
+        TRACE("pdr", tout << this << " " << 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 {
+            m_next->m_prev = m_prev;
+            m_prev->m_next = m_next;
+            if (this == root) {
+                root = m_next;
+            }
+        }
+        TRACE("pdr", tout << "new root: " << root << "\n";);
+        m_prev = 0;
+        m_next = 0;
+    }
+
+
+    void model_node::enqueue(model_node* n) {
+        TRACE("pdr", tout << n << " " << n->state() << "\n";);
+        SASSERT(!n->m_next);
+        SASSERT(!n->m_prev);
+        if (this == n) {
+            m_next = n;
+            m_prev = n;
+        }
+        else {
+            n->m_next = m_next;
+            m_next->m_prev = n;
+            m_next = n;
+            n->m_prev = this;
+        }
+    }
     // ----------------
     // model_search
 
+    /**
+       \brief Dequeue the next goal.
+     */
     model_node* model_search::next() {
-        if (m_leaves.empty()) {
+        if (!m_goal) {
             return 0;
         }
-        model_node* result = m_leaves.back();
-        m_leaves.pop_back();
-        return result;
+        else {
+            model_node* result = m_goal;
+            result->dequeue(m_goal);
+            return result;
+        }
     }
 
     bool model_search::is_repeated(model_node& n) const {
         model_node* p = n.parent();
         while (p) {
             if (p->state() == n.state()) {
+                TRACE("pdr", tout << "repeated\n";);
                 return true;
             }
             p = p->parent();
@@ -876,10 +937,15 @@ namespace pdr {
     }
 
     void model_search::add_leaf(model_node& n) {
+        SASSERT(n.children().empty());
         model_nodes ns;
         model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value;
+        if (nodes.contains(&n)) {
+            return;
+        }
         nodes.push_back(&n);
-        if (nodes.size() == 1 || is_repeated(n)) {
+        TRACE("pdr_verbose", tout << "add: " << n.level() << ": " << &n << " " << n.state() << "\n";);
+        if (nodes.size() == 1) {
             set_leaf(n);
         }
         else {
@@ -890,15 +956,21 @@ namespace pdr {
     void model_search::set_leaf(model_node& n) {
         erase_children(n, true);
         SASSERT(n.is_open());      
-        enqueue_leaf(n);
+        enqueue_leaf(&n);
     }
 
-    void model_search::enqueue_leaf(model_node& n) {
-        if (m_bfs) {
-            m_leaves.push_front(&n);
+    void model_search::enqueue_leaf(model_node* n) {
+        TRACE("pdr_verbose", tout << n << " " << n->state() << " goal: " << m_goal << "\n";);
+        SASSERT(n->is_open());        
+        if (!m_goal) {
+            m_goal = n;
+            m_goal->enqueue(n);
+        }
+        else if (m_bfs) {
+            m_goal->enqueue(n);
         }
         else {
-            m_leaves.push_back(&n);
+            m_goal->next()->enqueue(n);
         }
     }
 
@@ -921,56 +993,132 @@ namespace pdr {
     void model_search::erase_children(model_node& n, bool backtrack) {
         ptr_vector<model_node> todo, nodes;
         todo.append(n.children());
-        erase_leaf(n);
+        remove_goal(n);
         n.reset();
         while (!todo.empty()) {
             model_node* m = todo.back();
             todo.pop_back();
             nodes.push_back(m);
             todo.append(m->children());
-            erase_leaf(*m);
             remove_node(*m, backtrack);
         }
         std::for_each(nodes.begin(), nodes.end(), delete_proc<model_node>());
     }
 
     void model_search::remove_node(model_node& n, bool backtrack) {
+        TRACE("pdr_verbose", tout << "remove: " << n.level() << ": " << &n << " " << n.state() << "\n";);
         model_nodes& nodes = cache(n).find(n.state());
         nodes.erase(&n);
-        if (nodes.size() > 0 && n.is_open() && backtrack) {
-            for (unsigned i = 0; i < nodes.size(); ++i) {
-                nodes[i]->reopen();
-            }
+        bool is_goal = n.is_goal();
+        remove_goal(n);
+        if (!nodes.empty() && is_goal && backtrack) {
+            TRACE("pdr_verbose", for (unsigned i = 0; i < nodes.size(); ++i) n.display(tout << &n << "\n", 2););
+            model_node* n1 = nodes[0];
+            n1->set_open();
+            SASSERT(n1->children().empty());
+            enqueue_leaf(n1);
         }
         if (nodes.empty()) {            
             cache(n).remove(n.state());
         }
     }
 
-    void model_search::erase_leaf(model_node& n) {
-        if (n.children().empty() && n.is_open()) {
-            std::deque<model_node*>::iterator 
-                it  = m_leaves.begin(), 
-                end = m_leaves.end();
-            for (; it != end; ++it) {
-                if (*it == &n) {
-                    m_leaves.erase(it);
-                    break;
+    void model_search::remove_goal(model_node& n) {
+        n.dequeue(m_goal);        
+    }
+
+    void model_search::well_formed() {
+        // each open leaf is in the set of m_goal.
+        ptr_vector<model_node> nodes;
+        nodes.push_back(&get_root());
+        for (unsigned i = 0; i < nodes.size(); ++i) {
+            model_node* n = nodes[i];
+            if (!n->children().empty()) {
+                nodes.append(n->children());
+            }
+            else if (n->is_open() && !n->is_goal() && n->parent()) {
+                TRACE("pdr", n->display(tout << "node " << n << " not found among leaves\n", 0); display(tout););
+                UNREACHABLE();
+                return;
+            }
+        }
+        if (m_goal) {
+            model_node* n = m_goal;            
+            do {
+                if (!n->is_open() || !n->children().empty()) {
+                    TRACE("pdr", n->display(tout << "invalid leaf\n", 0); 
+                          display(tout););
+                    UNREACHABLE();
+                    return;
+                }                
+                n = n->next();
+            }
+            while (m_goal != n);
+        }
+
+        // each state appears in at most one goal per level.        
+        bool found = true;
+        for (unsigned l = 0; m_goal && found; ++l) {
+            found = false;
+            obj_hashtable<expr> open_states;            
+            model_node* n = m_goal;
+            do {
+                if (n->level() == l) {
+                    found = true;
+                    if (n->is_open()) {
+                        if (open_states.contains(n->state())) {
+                            TRACE("pdr", n->display(tout << "repeated leaf\n", 0); display(tout););
+                            UNREACHABLE();
+                        }
+                        open_states.insert(n->state());
+                    }
+                }
+                n = n->next();
+            }
+            while (m_goal != n);
+        }
+        // a node is open if and only if it contains an 
+        // open child which is a goal.
+        for (unsigned i = 0; i < nodes.size(); ++i) {
+            model_node* n = nodes[i];
+            if (!n->children().empty() && n->parent()) {
+                found = false;
+                for (unsigned j = 0; !found && j < n->children().size(); ++j) {
+                    found = n->children()[j]->is_open();
+                }
+                if (n->is_open() != found) {
+                    TRACE("pdr", n->display(tout << "node in inconsistent state\n", 0); display(tout););
+                    UNREACHABLE();
                 }
             }
         }
     }
 
+    unsigned model_search::num_goals() const {
+        model_node* n = m_goal;
+        unsigned num = 0;
+        if (n) {
+            do {
+                ++num;
+                n = n->next();
+            }
+            while (n != m_goal);
+        }
+        return num;
+    }
+
     std::ostream& model_search::display(std::ostream& out) const {
         if (m_root) {
             m_root->display(out, 0);
         }
-        out << "goals\n";
-        std::deque<model_node*>::const_iterator 
-            it  = m_leaves.begin(), 
-            end = m_leaves.end();
-        for (; it != end; ++it) {
-            (*it)->display(out, 1);
+        out << "goals " << num_goals() << "\n";
+        model_node* n = m_goal;
+        if (n) {
+            do {
+                n->display(out, 1);
+                n = n->next();
+            }
+            while (n != m_goal);
         }
         return out;
     }
@@ -1253,8 +1401,8 @@ namespace pdr {
             remove_node(*m_root, false);
             dealloc(m_root);
             m_root = 0;
-            m_cache.reset();
         }
+        m_cache.reset();
     }
 
     void model_search::backtrack_level(bool uses_level, model_node& n) {
@@ -1262,7 +1410,7 @@ namespace pdr {
         if (uses_level && m_root->level() > n.level()) {
             IF_VERBOSE(2, verbose_stream() << "Increase level " << n.level() << "\n";);
             n.increase_level();
-            enqueue_leaf(n);
+            enqueue_leaf(&n);
         }
         else {
             model_node* p = n.parent();
@@ -1270,15 +1418,16 @@ namespace pdr {
                 set_leaf(*p);
             }               
         }     
+        DEBUG_CODE(well_formed(););
     }
 
     // ----------------
     // context
 
     context::context(
-        smt_params&     fparams,
-        fixedpoint_params const&     params,
-        ast_manager&          m
+        smt_params&               fparams,
+        fixedpoint_params const&  params,
+        ast_manager&              m
         )
         : m_fparams(fparams),
           m_params(params),
@@ -1862,17 +2011,6 @@ namespace pdr {
         }
     }
 
-    void context::check_pre_closed(model_node& n) {
-        for (unsigned i = 0; i < n.children().size(); ++i) {
-            if (!n.children()[i]->is_closed()) return;
-        }
-        n.set_pre_closed();
-        model_node* p = n.parent();
-        while (p && p->is_1closed()) {
-            p->set_pre_closed();
-            p = p->parent();
-        }
-    }
 
     void context::expand_node(model_node& n) {
         SASSERT(n.is_open());
@@ -2143,10 +2281,10 @@ namespace pdr {
             model_node* child = alloc(model_node, &n, n_cube, pt, n.level()-1);
             ++m_stats.m_num_nodes;
             m_search.add_leaf(*child); 
-            IF_VERBOSE(3, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
+            IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(n_cube, m) << " " << (child->is_closed()?"closed":"open") << "\n";);
             m_stats.m_max_depth = std::max(m_stats.m_max_depth, child->depth());
         }
-        check_pre_closed(n);
+        n.check_pre_closed();
         TRACE("pdr", m_search.display(tout););
     }
 
diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h
index 44fba03d8..070a80ca4 100644
--- a/src/muz/pdr/pdr_context.h
+++ b/src/muz/pdr/pdr_context.h
@@ -186,6 +186,8 @@ namespace pdr {
     // structure for counter-example search.
     class model_node {
         model_node*            m_parent;
+        model_node*            m_next;
+        model_node*            m_prev;
         pred_transformer&      m_pt;
         expr_ref               m_state;
         model_ref              m_model;
@@ -197,13 +199,17 @@ namespace pdr {
         datalog::rule const*   m_rule;
     public:
         model_node(model_node* parent, expr_ref& state, pred_transformer& pt, unsigned level):
-            m_parent(parent), m_pt(pt), m_state(state), m_model(0), 
-                m_level(level), m_orig_level(level), m_depth(0), m_closed(false), m_rule(0) {
-            if (m_parent) {
-                m_parent->m_children.push_back(this);
-                SASSERT(m_parent->m_level == level+1);
-                SASSERT(m_parent->m_level > 0);
-                m_depth = m_parent->m_depth+1;
+            m_parent(parent), m_next(0), m_prev(0), m_pt(pt), m_state(state), m_model(0), 
+            m_level(level), m_orig_level(level), m_depth(0), m_closed(false), m_rule(0) {
+            model_node* p = m_parent;
+            if (p) {
+                p->m_children.push_back(this);
+                SASSERT(p->m_level == level+1);
+                SASSERT(p->m_level > 0);
+                m_depth = p->m_depth+1;
+                if (p && p->is_closed()) {
+                    p->set_open();
+                }
             }
         }
         void set_model(model_ref& m) { m_model = m; }
@@ -211,7 +217,7 @@ namespace pdr {
         unsigned orig_level() const { return m_orig_level; }
         unsigned depth() const { return m_depth; }
         void     increase_level() { ++m_level; }
-        expr*    state() const { return m_state; }
+        expr_ref const& state() const { return m_state; }
         ptr_vector<model_node> const& children() { return m_children; }
         pred_transformer& pt() const { return m_pt; }
         model_node* parent() const { return m_parent; }
@@ -231,8 +237,9 @@ namespace pdr {
             return true;
         }
 
+        void check_pre_closed();
         void set_closed();     
-        void reopen();
+        void set_open();
         void set_pre_closed() { m_closed = true; }
         void reset() { m_children.reset(); }
 
@@ -242,36 +249,45 @@ namespace pdr {
         void mk_instantiate(datalog::rule_ref& r0, datalog::rule_ref& r1, expr_ref_vector& binding);
 
         std::ostream& display(std::ostream& out, unsigned indent);
+
+        void dequeue(model_node*& root);
+        void enqueue(model_node* n);
+        model_node* next() const { return m_next; }
+        bool is_goal() const { return 0 != next(); }
     };
 
     class model_search {
         typedef ptr_vector<model_node> model_nodes;
         bool               m_bfs;
         model_node*        m_root;
-        std::deque<model_node*> m_leaves;
+        model_node*        m_goal;
         vector<obj_map<expr, model_nodes > > m_cache;
         obj_map<expr, model_nodes>& cache(model_node const& n);
         void erase_children(model_node& n, bool backtrack);
-        void erase_leaf(model_node& n);
         void remove_node(model_node& n, bool backtrack);
-        void enqueue_leaf(model_node& n); // add leaf to priority queue.
+        void enqueue_leaf(model_node* n); // add leaf to priority queue.
         void update_models();
+        void set_leaf(model_node& n); // Set node as leaf, remove children.
+        bool is_repeated(model_node& n) const;
+        unsigned num_goals() const; 
+
     public:
-        model_search(bool bfs): m_bfs(bfs), m_root(0) {}
+        model_search(bool bfs): m_bfs(bfs), m_root(0), m_goal(0) {}
         ~model_search();
 
         void reset();
         model_node* next();
-        bool is_repeated(model_node& n) const;
         void add_leaf(model_node& n); // add fresh node.
-        void set_leaf(model_node& n); // Set node as leaf, remove children.
-
+        
         void set_root(model_node* n);
         model_node& get_root() const { return *m_root; }
         std::ostream& display(std::ostream& out) const; 
         expr_ref get_trace(context const& ctx);        
         proof_ref get_proof_trace(context const& ctx);
         void backtrack_level(bool uses_level, model_node& n);
+        void remove_goal(model_node& n);
+
+        void well_formed();
     };
 
     struct model_exception { };
diff --git a/src/test/main.cpp b/src/test/main.cpp
index d5608a7d4..7b01e35c1 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -224,6 +224,7 @@ int main(int argc, char ** argv) {
     TST(theory_pb);
     TST(simplex);
     TST(sat_user_scope);
+    TST(pdr);
     //TST_ARGV(hs);
 }
 
diff --git a/src/test/pdr.cpp b/src/test/pdr.cpp
new file mode 100644
index 000000000..82448e6f5
--- /dev/null
+++ b/src/test/pdr.cpp
@@ -0,0 +1,116 @@
+#include "pdr_context.h"
+#include "reg_decl_plugins.h"
+
+
+using namespace pdr;
+
+static expr_ref mk_state(expr_ref_vector const& states, random_gen& rand) {
+    expr_ref result(states.get_manager());
+    result = states[rand(states.size())];
+    return result;
+}
+
+
+struct test_model_search {
+    struct init_test {
+        init_test(func_decl_ref& fn) {
+            ast_manager& m = fn.get_manager();
+            reg_decl_plugins(m);
+            fn = m.mk_const_decl(symbol("f"), m.mk_bool_sort());
+        }
+    };
+
+    ast_manager       m;
+    smt_params        smt_params;
+    fixedpoint_params fp_params;
+    context           ctx;
+    manager           pm;
+    func_decl_ref     fn;
+    init_test         initt;
+    pred_transformer  pt;
+    random_gen        rand;
+    model_search      search;
+    expr_ref_vector   states;  
+
+
+    test_model_search():
+        ctx(smt_params, fp_params, m),
+        pm(smt_params, 10, m),
+        fn(m),
+        initt(fn),
+        pt(ctx, pm, fn),
+        rand(10),
+        search(true),
+        states(m) {
+    }
+
+    void add_tree(model_node* parent, bool force_goal) {
+        unsigned level = parent->level();
+        search.add_leaf(*parent);
+        if (level > 0 && (force_goal || parent->is_goal())) {
+            search.remove_goal(*parent);
+            add_tree(alloc(model_node, parent, mk_state(states, rand), pt, level-1), false);
+            add_tree(alloc(model_node, parent, mk_state(states, rand), pt, level-1), false);
+            parent->check_pre_closed();
+        }
+    }
+
+    bool mutate() {
+        model_node* leaf = search.next();
+        if (!leaf) return false;
+        unsigned level = leaf->level();
+        if (level == 0) {
+            if (rand(2) == 0) {
+                leaf->display(std::cout << "backtrack to grandparent\n", 1);
+                search.backtrack_level(false, *leaf->parent());
+            }
+            else {
+                leaf->display(std::cout << "backtrack to parent\n", 1);
+                search.backtrack_level(false, *leaf);
+            }
+        }
+        else {
+            leaf->display(std::cout << "grow tree\n", 1);
+            add_tree(leaf, true);
+        }
+        return true;
+    }
+
+    void init() {
+        std::cout << "pdr state-hash search tree\n";
+        
+        expr_ref state(m);
+        func_decl_ref fn(m);
+        for (unsigned i = 0; i < 10; ++i) {
+            std::ostringstream strm;
+            strm << "s" << i;
+            state = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort());
+            fn = to_app(state)->get_decl();
+            states.push_back(state);
+        }
+        state = states[0].get();
+        unsigned level = 4;
+        for(unsigned n = 0; n < 100; ++n) {
+            model_node* root = alloc(model_node, 0, mk_state(states, rand), pt, level);
+            search.set_root(root);
+            add_tree(root, false);
+            search.display(std::cout);
+            
+            while (true) {
+                search.well_formed();
+                if (!mutate()) break;
+                search.display(std::cout);
+            }
+            search.reset();
+            //++level;
+        }
+        search.reset();        
+    }
+
+};
+
+void tst_pdr() {
+    test_model_search test;
+
+    test.init();
+}