diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index bc32e14eb..05425c61b 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -2363,6 +2363,39 @@ expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) {
 	return n;
 }
 
+/*
+ * Look through the equivalence class of n to find an integer constant.
+ * Return that constant if it is found. Otherwise, return -1.
+ * Note that a return value of -1 should not normally be possible, as
+ * string length cannot be negative.
+ */
+
+rational theory_str::get_len_value(expr * n) {
+    ast_manager & m = get_manager();
+    context & ctx = get_context();
+    ctx.internalize(n, false);
+
+    TRACE("t_str_detail", tout << "checking eqc of " << mk_ismt2_pp(n, m) << " for an integer constant" << std::endl;);
+
+    enode * nNode = ctx.get_enode(n);
+    enode * eqcNode = nNode;
+    do {
+        app * ast = eqcNode->get_owner();
+        rational val;
+        bool is_int;
+        if (m_autil.is_numeral(n, val, is_int)) {
+            if (is_int) {
+                TRACE("t_str_detail", tout << "eqc contains integer constant " << val << std::endl;);
+                SASSERT(!val.is_neg());
+                return val;
+            }
+        }
+    } while (eqcNode != nNode);
+    // not found
+    TRACE("t_str_detail", tout << "eqc contains no integer constants" << std::endl;);
+    return rational(-1);
+}
+
 /*
  * Decide whether n1 and n2 are already in the same equivalence class.
  * This only checks whether the core considers them to be equal;
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 3bb3940b6..cf7ef0060 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -146,6 +146,8 @@ namespace smt {
         expr * get_eqc_value(expr * n, bool & hasEqcValue);
         bool in_same_eqc(expr * n1, expr * n2);
 
+        rational get_len_value(expr * n);
+
         bool can_two_nodes_eq(expr * n1, expr * n2);
         bool can_concat_eq_str(expr * concat, std::string str);
         bool can_concat_eq_concat(expr * concat1, expr * concat2);