diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 325d6adcc..edb34bba7 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -9175,7 +9175,7 @@ namespace smt {
         } // RegexAutomata
 
         bool needToAssignFreeVars = false;
-        std::set<expr*> free_variables;
+        expr_ref_vector free_variables(m);
         std::set<expr*> unused_internal_variables;
         { // Z3str2 free variables check
             std::map<expr*, int>::iterator itor = varAppearInAssign.begin();
@@ -9196,7 +9196,7 @@ namespace smt {
                 if (!hasEqcValue) {
                     TRACE("str", tout << "found free variable " << mk_pp(itor->first, m) << std::endl;);
                     needToAssignFreeVars = true;
-                    free_variables.insert(itor->first);
+                    free_variables.push_back(itor->first);
                     // break;
                 } else {
                     // debug
@@ -9413,7 +9413,7 @@ namespace smt {
 
             expr_ref_vector precondition(m);
             expr_ref_vector cex(m);
-            lbool model_status = fixed_length_model_construction(assignments, precondition, candidate_model, cex);
+            lbool model_status = fixed_length_model_construction(assignments, precondition, free_variables, candidate_model, cex);
 
             if (model_status == l_true) {
                 m_stats.m_solved_by = 2;
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 2e31e4303..15e3a85d5 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -842,6 +842,7 @@ protected:
     bool finalcheck_int2str(app * a);
 
     lbool fixed_length_model_construction(expr_ref_vector formulas, expr_ref_vector &precondition,
+            expr_ref_vector& free_variables,
             obj_map<expr, zstring> &model, expr_ref_vector &cex);
     ptr_vector<expr> fixed_length_reduce_string_term(smt::kernel & subsolver, expr * term);
     bool fixed_length_get_len_value(expr * e, rational & val);
diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index d0bc6bc20..59f96cc80 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -614,6 +614,7 @@ namespace smt {
     }
 
     lbool theory_str::fixed_length_model_construction(expr_ref_vector formulas, expr_ref_vector &precondition,
+            expr_ref_vector& free_variables,
             obj_map<expr, zstring> &model, expr_ref_vector &cex) {
 
         ast_manager & m = get_manager();
@@ -658,6 +659,15 @@ namespace smt {
         sort * str_sort = u.str.mk_string_sort();
         sort * bool_sort = m.mk_bool_sort();
 
+        for (expr * var : free_variables) {
+            TRACE("str_fl", tout << "initialize free variable " << mk_pp(var, m) << std::endl;);
+            rational var_lenVal;
+            if (!fixed_length_get_len_value(var, var_lenVal)) {
+                NOT_IMPLEMENTED_YET();
+            }
+            fixed_length_reduce_string_term(subsolver, var);
+        }
+
         for (expr * f : formulas) {
             if (!get_context().is_relevant(f)) {
                 TRACE("str_fl", tout << "skip reducing formula " << mk_pp(f, m) << ", not relevant" << std::endl;);