diff --git a/lib/pdr_farkas_learner.cpp b/lib/pdr_farkas_learner.cpp
index e7b0bca33..5586fa2ca 100644
--- a/lib/pdr_farkas_learner.cpp
+++ b/lib/pdr_farkas_learner.cpp
@@ -514,7 +514,7 @@ namespace pdr {
 
         proof_ref pr(root, m);
         proof_utils::reduce_hypotheses(pr);
-        IF_VERBOSE(2, verbose_stream() << "Elim Hyps:\n" << mk_ismt2_pp(pr, m) << "\n";);
+        IF_VERBOSE(3, verbose_stream() << "Elim Hyps:\n" << mk_ismt2_pp(pr, m) << "\n";);
         proof_utils::permute_unit_resolution(pr);
         
         ptr_vector<expr_set> hyprefs;
diff --git a/lib/pdr_generalizers.cpp b/lib/pdr_generalizers.cpp
index 445b60665..a7f1922b4 100644
--- a/lib/pdr_generalizers.cpp
+++ b/lib/pdr_generalizers.cpp
@@ -105,14 +105,14 @@ namespace pdr {
             lit = core[i].get();
             core[i] = m.mk_true();
             state = m.mk_not(n.pt().get_pdr_manager().mk_and(core));
-            bool assumes_level = false;
-            if (n.pt().is_invariant(n.level(), state, true, assumes_level, 0)) {
+            bool uses_level_tmp = false;
+            if (n.pt().is_invariant(n.level(), state, true, uses_level_tmp, 0)) {
                 num_failures = 0;
                 core[i] = core.back();
                 core.pop_back();
                 TRACE("pdr", tout << "Remove: " << mk_pp(lit, m) << "\n";);
                 ++num_changes;
-                uses_level = assumes_level;
+                uses_level = uses_level_tmp;
             }
             else {
                 core[i] = lit;
@@ -120,6 +120,7 @@ namespace pdr {
                 ++i;
             }
         }
+        IF_VERBOSE(1, verbose_stream() << "changes: " << num_changes << " size: " << core.size() << "\n";);
         TRACE("pdr", tout << "changes: " << num_changes << " index: " << i << " size: " << core.size() << "\n";);
     }