diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index e23915ab4..75ee20ebd 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -73,5 +73,6 @@ def_module_params(module_name='smt',
                           ('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'),
                           ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'),
                           ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
-                          ('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement')
+                          ('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement'),
+                          ('str.overlap_priority', DOUBLE, -0.1, 'theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true')
                           ))
diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp
index 46302cf82..f86cd9379 100644
--- a/src/smt/params/theory_str_params.cpp
+++ b/src/smt/params/theory_str_params.cpp
@@ -30,4 +30,5 @@ void theory_str_params::updt_params(params_ref const & _p) {
     m_FiniteOverlapModels = p.str_finite_overlap_models();
     m_UseBinarySearch = p.str_use_binary_search();
     m_BinarySearchInitialUpperBound = p.str_binary_search_start();
+    m_OverlapTheoryAwarePriority = p.str_overlap_priority();
 }
diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h
index 4effb0897..de0945395 100644
--- a/src/smt/params/theory_str_params.h
+++ b/src/smt/params/theory_str_params.h
@@ -78,6 +78,8 @@ struct theory_str_params {
     bool m_UseBinarySearch;
     unsigned m_BinarySearchInitialUpperBound;
 
+    double m_OverlapTheoryAwarePriority;
+
     theory_str_params(params_ref const & p = params_ref()):
         m_AssertStrongerArrangements(true),
         m_AggressiveLengthTesting(false),
@@ -88,7 +90,8 @@ struct theory_str_params {
         m_StringConstantCache(true),
         m_FiniteOverlapModels(false),
         m_UseBinarySearch(false),
-        m_BinarySearchInitialUpperBound(64)
+        m_BinarySearchInitialUpperBound(64),
+        m_OverlapTheoryAwarePriority(-0.1)
     {
         updt_params(p);
     }
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 706f2cd73..138b7db9f 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -3249,7 +3249,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
             if (m_params.m_FiniteOverlapModels) {
                 expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2);
                 assert_implication(ax_l, tester);
-                add_theory_aware_branching_info(tester, -0.1, l_true);
+                add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true);
             } else {
                 TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
                 // TODO printCutVar(m, y);
@@ -3307,7 +3307,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
             if (m_params.m_FiniteOverlapModels) {
                 expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2);
                 assert_implication(ax_l, tester);
-                add_theory_aware_branching_info(tester, -0.1, l_true);
+                add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true);
             } else {
                 TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
                 // TODO printCutVar(m, y);
@@ -3361,7 +3361,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
             if (m_params.m_FiniteOverlapModels) {
                 expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2);
                 arrangement_disjunction.push_back(tester);
-                add_theory_aware_branching_info(tester, -0.1, l_true);
+                add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true);
             } else {
                 TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
                 TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);});
@@ -3406,7 +3406,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
                 // TODO this might repeat the case above, we may wish to avoid doing this twice
                 expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2);
                 arrangement_disjunction.push_back(tester);
-                add_theory_aware_branching_info(tester, -0.1, l_true);
+                add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true);
             } else {
                 TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
                 // TODO printCutVar(x, n);
@@ -3645,7 +3645,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
 	            if (m_params.m_FiniteOverlapModels) {
 	                expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2);
                     assert_implication(ax_l, tester);
-                    add_theory_aware_branching_info(tester, -0.1, l_true);
+                    add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true);
 	            } else {
 	                TRACE("t_str", tout << "AVOID LOOP: SKIP" << std::endl;);
 	                // TODO printCutVar(m, y);
@@ -3753,7 +3753,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
 				if (m_params.m_FiniteOverlapModels) {
 				    expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2);
                     arrangement_disjunction.push_back(tester);
-                    add_theory_aware_branching_info(tester, -0.1, l_true);
+                    add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true);
 				} else {
 				    TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
 				    // TODO printCutVar(m, y)
@@ -4046,7 +4046,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
                 if (m_params.m_FiniteOverlapModels) {
                     expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2);
                     assert_implication(ax_l, tester);
-                    add_theory_aware_branching_info(tester, -0.1, l_true);
+                    add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true);
                 } else {
                     TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
                     // TODO printCutVar(x, n);
@@ -4126,7 +4126,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
                 if (m_params.m_FiniteOverlapModels) {
                     expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2);
                     arrangement_disjunction.push_back(tester);
-                    add_theory_aware_branching_info(tester, -0.1, l_true);
+                    add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true);
                 } else {
                     TRACE("t_str", tout << "AVOID LOOP: SKIPPED." << std::endl;);
                     // TODO printCutVAR(x, n)
@@ -4532,7 +4532,7 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) {
         if (m_params.m_FiniteOverlapModels) {
             expr_ref tester = set_up_finite_model_test(concatAst1, concatAst2);
             arrangement_disjunction.push_back(tester);
-            add_theory_aware_branching_info(tester, -0.1, l_true);
+            add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true);
         } else {
             TRACE("t_str", tout << "AVOID LOOP: SKIPPED." << std::endl;);
             TRACE("t_str", print_cut_var(m, tout); print_cut_var(y, tout););