diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index f8366ed07..02db2132a 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -30,6 +30,7 @@ theory_str::theory_str(ast_manager & m):
         /* Options */
         opt_AggressiveLengthTesting(true),
         opt_AggressiveValueTesting(true),
+        opt_EagerStringConstantLengthAssertions(true),
         /* Internal setup */
         search_started(false),
         m_autil(m),
@@ -191,7 +192,9 @@ bool theory_str::internalize_term(app * term) {
     //}
     */
 
-    // from theory_seq::internalize_term()
+    // TODO do we still need to do instantiate_concat_axiom()?
+
+    // partially from theory_seq::internalize_term()
     if (ctx.e_internalized(term)) {
         enode* e = ctx.get_enode(term);
         mk_var(e);
@@ -217,6 +220,12 @@ bool theory_str::internalize_term(app * term) {
     else {
         e = ctx.mk_enode(term, false, m.is_bool(term), true);
     }
+
+    if (opt_EagerStringConstantLengthAssertions && m_strutil.is_string(term)) {
+        TRACE("t_str", tout << "eagerly asserting length of string term " << mk_pp(term, m) << std::endl;);
+        m_basicstr_axiom_todo.insert(e);
+    }
+
     theory_var v = mk_var(e);
     TRACE("t_str_detail", tout << "term " << mk_ismt2_pp(term, get_manager()) << " = v#" << v << std::endl;);
 
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 99899b365..2b8077a13 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -74,6 +74,15 @@ namespace smt {
          */
         bool opt_AggressiveValueTesting;
 
+        /*
+         * Setting EagerStringConstantLengthAssertions to true allows some methods,
+         * in particular internalize_term(), to add
+         * length assertions about relevant string constants.
+         * Note that currently this should always be set to 'true', or else *no* length assertions
+         * will be made about string constants.
+         */
+        bool opt_EagerStringConstantLengthAssertions;
+
         bool search_started;
         arith_util m_autil;
         str_util m_strutil;
@@ -87,6 +96,7 @@ namespace smt {
         ptr_vector<enode> m_basicstr_axiom_todo;
         svector<std::pair<enode*,enode*> > m_str_eq_todo;
         ptr_vector<enode> m_concat_axiom_todo;
+        ptr_vector<enode> m_string_constant_length_todo;
 
         int tmpStringVarCount;
         int tmpXorVarCount;