diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 39e519863..a55d0e648 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -929,7 +929,7 @@ namespace pdr {
         model_node* p = n.parent();
         while (p) {
             if (p->state() == n.state()) {
-                TRACE("pdr", tout << "repeated\n";);
+                TRACE("pdr", tout << n.state() << "repeated\n";);
                 return true;
             }
             p = p->parent();
@@ -1019,6 +1019,11 @@ namespace pdr {
             SASSERT(n1->children().empty());
             enqueue_leaf(n1);
         }
+
+        if (!nodes.empty() && n.get_model_ptr() && backtrack) {
+            model_ref mr(n.get_model_ptr());
+            nodes[0]->set_model(mr);
+        }
         if (nodes.empty()) {            
             cache(n).remove(n.state());
         }