diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp
index ed9e4d999..8e15fa983 100644
--- a/src/muz_qe/pdr_generalizers.cpp
+++ b/src/muz_qe/pdr_generalizers.cpp
@@ -364,6 +364,7 @@ namespace pdr {
         }
         vector<unsigned_vector> transversal;
         while (l_true == ctx.check()) {
+            IF_VERBOSE(0, ctx.display(verbose_stream()););
             model_ref md;
             ctx.get_model(md);
             expr_ref_vector lits(m);
diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp
index d597500b2..75f68c7f1 100644
--- a/src/muz_qe/rel_context.cpp
+++ b/src/muz_qe/rel_context.cpp
@@ -105,6 +105,11 @@ namespace datalog {
         }        
     }
 
+    lbool rel_context::saturate() {
+        scoped_query sq(m_context);
+        return saturate(sq);
+    }
+
     lbool rel_context::saturate(scoped_query& sq) {
         m_context.ensure_closed();        
         bool time_limit = m_context.soft_timeout()!=0;
diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h
index 0b73caaa6..20da827ce 100644
--- a/src/muz_qe/rel_context.h
+++ b/src/muz_qe/rel_context.h
@@ -48,6 +48,8 @@ namespace datalog {
         
         void reset_tables();
 
+        lbool saturate(scoped_query& sq);
+
     public:
         rel_context(context& ctx);
 
@@ -109,7 +111,7 @@ namespace datalog {
 
         void display_profile(std::ostream& out);
 
-        lbool saturate(scoped_query& sq);
+        lbool saturate();
 
     };
 };