diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index ca1abde3f..fb798fd26 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1795,6 +1795,8 @@ struct contains_underspecified_op_proc {
             throw found();
         if (m_arith.is_non_algebraic(n))
             throw found();
+        if (m_arith.is_irrational_algebraic_numeral(n))
+            throw found();
         if (n->get_family_id() == m_array_fid) {
             decl_kind k = n->get_decl_kind();
             if (k == OP_AS_ARRAY ||
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 90ca58980..a29a5c595 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -110,7 +110,6 @@ class propagate_values_tactic : public tactic {
         expr * curr = m_goal->form(m_idx);
         expr_ref   new_curr(m);
         proof_ref  new_pr(m);
-        std::cout << m_goal->pr(m_idx) << "\n";
         
         if (!m_subst->empty()) {
             m_r(curr, new_curr, new_pr);