diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 1fc06b079..23c102874 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -472,8 +472,7 @@ class theory_lra::imp {
                 else if (a.is_mod(n, n1, n2)) {
                     if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
                     if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2);
-                    if (a.is_numeral(n2) && !r.is_zero()) {
-                        ensure_nla();
+                    if (m_nla && a.is_numeral(n2) && !r.is_zero()) {
                         app_ref div(a.mk_idiv(n1, n2), m);
                         ctx().internalize(div, false);
                         internalize_term(to_app(div));
diff --git a/src/test/mod_factor.cpp b/src/test/mod_factor.cpp
index 68aeab7dd..069802522 100644
--- a/src/test/mod_factor.cpp
+++ b/src/test/mod_factor.cpp
@@ -10,17 +10,18 @@ Copyright (c) 2025 Microsoft Corporation
 static void test_mod_factor_mod_path() {
     Z3_config cfg = Z3_mk_config();
     Z3_context ctx = Z3_mk_context(cfg);
-    Z3_solver s = Z3_mk_solver(ctx);
+    Z3_solver s = Z3_mk_solver_for_logic(ctx, Z3_mk_string_symbol(ctx, "QF_NIA"));
     Z3_solver_inc_ref(ctx, s);
     Z3_sort int_sort = Z3_mk_int_sort(ctx);
     Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), int_sort);
     Z3_ast y = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "y"), int_sort);
     Z3_ast seven = Z3_mk_int(ctx, 7, int_sort);
     Z3_ast zero = Z3_mk_int(ctx, 0, int_sort);
-    Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_mod(ctx, x, seven), zero));
     Z3_ast xy_args[] = {x, y};
     Z3_ast xy = Z3_mk_mul(ctx, 2, xy_args);
+    // assert mul term first so ensure_nla() fires before mod internalization
     Z3_solver_assert(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, Z3_mk_mod(ctx, xy, seven), zero)));
+    Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_mod(ctx, x, seven), zero));
     ENSURE(Z3_solver_check(ctx, s) == Z3_L_FALSE);
     Z3_solver_dec_ref(ctx, s);
     Z3_del_config(cfg);
@@ -33,7 +34,7 @@ static void test_mod_factor_mod_path() {
 static void test_mod_factor_idiv_path() {
     Z3_config cfg = Z3_mk_config();
     Z3_context ctx = Z3_mk_context(cfg);
-    Z3_solver s = Z3_mk_solver(ctx);
+    Z3_solver s = Z3_mk_solver_for_logic(ctx, Z3_mk_string_symbol(ctx, "QF_NIA"));
     Z3_solver_inc_ref(ctx, s);
     Z3_sort int_sort = Z3_mk_int_sort(ctx);
     Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), int_sort);
@@ -43,9 +44,7 @@ static void test_mod_factor_idiv_path() {
     Z3_ast hundred = Z3_mk_int(ctx, 100, int_sort);
     // xm = x mod 100 (bounded by is_bounded)
     Z3_ast xm = Z3_mk_mod(ctx, x, hundred);
-    // xm mod 7 = 0
-    Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_mod(ctx, xm, seven), zero));
-    // (xm * y) div 7 — triggers idiv internalization with bounded dividend
+    // (xm * y) — assert mul term first so ensure_nla() fires before mod internalization
     Z3_ast xm_y_args[] = {xm, y};
     Z3_ast xm_y = Z3_mk_mul(ctx, 2, xm_y_args);
     Z3_ast xm_y_div = Z3_mk_div(ctx, xm_y, seven);
@@ -53,6 +52,8 @@ static void test_mod_factor_idiv_path() {
     Z3_solver_assert(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, Z3_mk_mod(ctx, xm_y, seven), zero)));
     // use div to keep it alive
     Z3_solver_assert(ctx, s, Z3_mk_ge(ctx, xm_y_div, zero));
+    // xm mod 7 = 0
+    Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_mod(ctx, xm, seven), zero));
     ENSURE(Z3_solver_check(ctx, s) == Z3_L_FALSE);
     Z3_solver_dec_ref(ctx, s);
     Z3_del_config(cfg);