diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp
index 518da6804..0f6b7e4cb 100644
--- a/src/smt/theory_str_regex.cpp
+++ b/src/smt/theory_str_regex.cpp
@@ -93,7 +93,8 @@ namespace smt {
                         // generate new length constraint
                         expr_ref_vector extra_length_vars(m);
                         expr_ref _top_level_length_constraint = infer_all_regex_lengths(mk_strlen(str), re, extra_length_vars);
-                        expr_ref top_level_length_constraint(_top_level_length_constraint, m);
+                        expr_ref premise(str_in_re, m);
+                        expr_ref top_level_length_constraint(m.mk_implies(premise, _top_level_length_constraint), m);
                         th_rewriter rw(m);
                         rw(top_level_length_constraint);
                         TRACE("str", tout << "top-level length constraint: " << mk_pp(top_level_length_constraint, m) << std::endl;);