diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 509e15ff7..f97397108 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -429,7 +429,7 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
     if ((get_sutil().is_seq(s) || get_sutil().is_re(s)) && !get_sutil().is_string(s)) {
         ptr_buffer<format> fs;
         fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast())));
-        return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"Re");
+        return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"RegEx");
     }
 #if 0
     if (get_dtutil().is_datatype(s)) {
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 2e928af37..89e0123a8 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -4653,34 +4653,24 @@ namespace smt {
     }
 
     bool theory_str::get_arith_value(expr* e, rational& val) const {
-        if (opt_DisableIntegerTheoryIntegration) {
-            TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;);
-            return false;
-        }
-
         context& ctx = get_context();
         ast_manager & m = get_manager();
-        theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
-        if (!tha) {
+
+	// safety
+	if (!ctx.e_internalized(e)) {
+	  return false;
+	}
+	
+        // if an integer constant exists in the eqc, it should be the root
+        enode * en_e = ctx.get_enode(e);
+        enode * root_e = en_e->get_root();
+        if (m_autil.is_numeral(root_e->get_owner(), val) && val.is_int()) {
+            TRACE("str", tout << mk_pp(e, m) << " ~= " << mk_pp(root_e->get_owner(), m) << std::endl;);
+            return true;
+        } else {
+            TRACE("str", tout << "root of eqc of " << mk_pp(e, m) << " is not a numeral" << std::endl;);
             return false;
         }
-        TRACE("str", tout << "checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;);
-        expr_ref _val(m);
-        enode * en_e = ctx.get_enode(e);
-        enode * it = en_e;
-        do {
-            if (m_autil.is_numeral(it->get_owner(), val) && val.is_int()) {
-                // found an arithmetic term
-                TRACE("str", tout << mk_pp(it->get_owner(), m) << " is an integer ( ~= " << val << " )"
-                      << std::endl;);
-                return true;
-            } else {
-                TRACE("str", tout << mk_pp(it->get_owner(), m) << " not a numeral" << std::endl;);
-            }
-            it = it->get_next();
-        } while (it != en_e);
-        TRACE("str", tout << "no arithmetic values found in eqc" << std::endl;);
-        return false;
     }
 
     bool theory_str::lower_bound(expr* _e, rational& lo) {