diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index c8c5adc3c..6f4963990 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -269,17 +269,16 @@ namespace arith {
                 }
                 else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) {
                     found_unsupported(n);
+                    ensure_arg_vars(to_app(n));
                 }
                 else {
-                    // no-op
+                    ensure_arg_vars(to_app(n));
                 }
             }
             else {
                 if (is_app(n)) {
                     internalize_args(to_app(n));
-                    for (expr* arg : *to_app(n)) 
-                        if (a.is_real(arg) || a.is_int(arg))
-                            internalize_term(arg);
+                    ensure_arg_vars(to_app(n));
                 }
                 theory_var v = mk_evar(n);
                 coeffs[vars.size()] = coeffs[index];
@@ -426,6 +425,12 @@ namespace arith {
             e_internalize(arg);
     }
 
+    void solver::ensure_arg_vars(app* n) {
+        for (expr* arg : *to_app(n))
+            if (a.is_real(arg) || a.is_int(arg))
+                internalize_term(arg);
+    }
+
     theory_var solver::internalize_power(app* t, app* n, unsigned p) {
         internalize_args(t, true);
         bool _has_var = has_var(t);
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 7fc4f3441..b6d6dbef8 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -239,6 +239,7 @@ namespace arith {
         void add_def_constraint(lp::constraint_index index, theory_var v);
         void add_def_constraint_and_equality(lpvar vi, lp::lconstraint_kind kind, const rational& bound);
         void internalize_args(app* t, bool force = false);
+        void ensure_arg_vars(app* t);
         theory_var internalize_power(app* t, app* n, unsigned p);
         theory_var internalize_mul(app* t);
         theory_var internalize_def(expr* term);