diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index a6f91a0a2..77b74336e 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -2662,6 +2662,12 @@ class RatNumRef(ArithRef):
         return self.denominator().as_long()
 
     def is_int(self):
+        return False
+
+    def is_real(self):
+        return True
+
+    def is_int_value(self):
         return self.denominator().is_int() and self.denominator_as_long() == 1
 
     def as_long(self):
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index c42572f1e..62fb99a11 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -896,7 +896,7 @@ namespace sat {
                 unsigned idx = l.index();
                 if (m_queue.contains(idx))
                     m_queue.decreased(idx);
-                else
+                else 
                     m_queue.insert(idx);
             }
             literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); }
@@ -918,16 +918,19 @@ namespace sat {
         }
 
         void insert(literal l) {
-            bool_var v = l.var();
-            if (s.is_external(v) || s.was_eliminated(v))
-                return;
             m_queue.insert(l);
         }
 
+        bool process_var(bool_var v) {
+            return !s.is_external(v) && !s.was_eliminated(v);
+        }
+
         void operator()(unsigned num_vars) {
             for (bool_var v = 0; v < num_vars; v++) {
-                insert(literal(v, false));
-                insert(literal(v, true));
+                if (process_var(v)) {
+                    insert(literal(v, false));
+                    insert(literal(v, true));
+                }
             }
             while (!m_queue.empty()) {
                 s.checkpoint();
@@ -941,9 +944,9 @@ namespace sat {
         void process(literal l) {
             TRACE("blocked_clause", tout << "processing: " << l << "\n";);
             model_converter::entry * new_entry = 0;
-            if (s.is_external(l.var()) || s.was_eliminated(l.var()))
+            if (!process_var(l.var())) {
                 return;
-
+            }
             {
                 m_to_remove.reset();
                 {
@@ -963,8 +966,10 @@ namespace sat {
                             mc.insert(*new_entry, c);
                             unsigned sz = c.size();
                             for (unsigned i = 0; i < sz; i++) {
-                                if (c[i] != l)
-                                    m_queue.decreased(~c[i]);
+                                literal lit = c[i];
+                                if (lit != l && process_var(lit.var())) {
+                                    m_queue.decreased(~lit);
+                                }
                             }
                         }
                         s.unmark_all(c);
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 178b2117f..a3f163ed4 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -63,5 +63,6 @@ def_module_params(module_name='smt',
                           ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
                           ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
                           ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
-                          ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances')
+                          ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
+                          ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core')
                           ))
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index f80ff09f4..ab6be5d91 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -37,6 +37,7 @@ namespace smt {
         symbol               m_logic;
         bool                 m_minimizing_core;
         bool                 m_core_extend_patterns;
+        unsigned             m_core_extend_patterns_max_distance;
         obj_map<expr, expr*> m_name2assertion;
 
     public:
@@ -46,12 +47,14 @@ namespace smt {
             m_params(p),
             m_context(m, m_smt_params),
             m_minimizing_core(false),
-            m_core_extend_patterns(false) {
+            m_core_extend_patterns(false),
+            m_core_extend_patterns_max_distance(UINT_MAX) {
             m_logic = l;
             if (m_logic != symbol::null)
                 m_context.set_logic(m_logic);
             smt_params_helper smth(p);
             m_core_extend_patterns = smth.core_extend_patterns();
+            m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance();
         }
 
         virtual solver * translate(ast_manager & m, params_ref const & p) {
@@ -283,7 +286,7 @@ namespace smt {
             func_decl_set pattern_fds;
             vector<func_decl_set> assrtn_fds;
 
-            do {
+            for (unsigned d = 0; d < m_core_extend_patterns_max_distance; d++) {
                 new_core_literals.reset();
 
                 unsigned sz = core.size();
@@ -308,8 +311,10 @@ namespace smt {
                 }
 
                 core.append(new_core_literals.size(), new_core_literals.c_ptr());
+
+                if (new_core_literals.empty())
+                    break;
             }
-            while (!new_core_literals.empty());
         }
     };
 };