diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 01f4f924f..dc1931bac 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1423,37 +1423,10 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
 }
 
 /*
- * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn))
+ * (re.range c_1 c_n) 
  */
 br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
     return BR_FAILED;
-    TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";);
-    zstring str_lo, str_hi;
-    if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) {
-        if (str_lo.length() == 1 && str_hi.length() == 1) {
-            unsigned int c1 = str_lo[0];
-            unsigned int c2 = str_hi[0];
-            if (c1 > c2) {
-                // exchange c1 and c2
-                unsigned int tmp = c1;
-                c2 = c1;
-                c1 = tmp;
-            }
-            zstring s(c1);
-            expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m());
-            for (unsigned int ch = c1 + 1; ch <= c2; ++ch) {
-                zstring s_ch(ch);
-                expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m());
-                acc = m_util.re.mk_union(acc, acc2);
-            }
-            result = acc;
-            return BR_REWRITE2;
-        } else {
-            m().raise_exception("string constants in re.range must have length 1");
-        }
-    }
-
-    return BR_FAILED;
 }
 
 /*
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 7a9369fd3..3f8845546 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2176,6 +2176,8 @@ bool theory_seq::simplify_and_solve_eqs() {
     return m_new_propagation || ctx.inconsistent();
 }
 
+void theory_seq::internalize_eq_eh(app * atom, bool_var v) {}
+
 
 bool theory_seq::internalize_term(app* term) {
     context & ctx   = get_context();
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 2b8fb2fd7..e145d3077 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -343,7 +343,7 @@ namespace smt {
         virtual final_check_status final_check_eh();
         virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); }
         virtual bool internalize_term(app*);
-        virtual void internalize_eq_eh(app * atom, bool_var v) {}
+        virtual void internalize_eq_eh(app * atom, bool_var v);
         virtual void new_eq_eh(theory_var, theory_var);
         virtual void new_diseq_eh(theory_var, theory_var);
         virtual void assign_eh(bool_var v, bool is_true);        
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 655f307c3..bd0fe8fac 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -62,7 +62,6 @@ class lar_solver : public column_namer {
     vector<lar_term*> m_terms;
     const var_index m_terms_start_index;
     indexed_vector<mpq> m_column_buffer;    
-    std::function<column_type (unsigned)> m_column_type_function;    
 public:
     lar_core_solver m_mpq_lar_core_solver;
     unsigned constraint_count() const;
diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h
index 6b80c2257..ad1a59f5a 100644
--- a/src/util/lp/mps_reader.h
+++ b/src/util/lp/mps_reader.h
@@ -655,7 +655,7 @@ class mps_reader {
       sense   interval
       G   [rhs, rhs + |range|]
       L   [rhs - |range|, rhs]
-      E   [rhs, rhs + |range|]     if range ¡Ý 0 [rhs - |range|, rhs]     if range < 0
+      E   [rhs, rhs + |range|]     if range in [rhs - |range|, rhs]     if range < 0
       where |range| is range's absolute value.
     */