From eed87807c5a7efaeabc67544a30671157c88c673 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Jun 2021 10:41:10 -0700
Subject: [PATCH] #5324

---
 src/sat/smt/arith_internalize.cpp | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index f27edfe06..498e6f725 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -275,6 +275,9 @@ namespace arith {
             else {
                 if (is_app(n)) {
                     internalize_args(to_app(n));
+                    for (expr* arg : *to_app(n)) 
+                        if (a.is_arith_expr(arg))
+                            internalize_term(arg);
                 }
                 theory_var v = mk_evar(n);
                 coeffs[vars.size()] = coeffs[index];
@@ -291,9 +294,8 @@ namespace arith {
         st.to_ensure_enode().reset();
         for (unsigned i = st.to_ensure_var().size(); i-- > 0; ) {
             expr* n = st.to_ensure_var()[i];
-            if (is_app(n)) {
+            if (is_app(n)) 
                 internalize_term(to_app(n));
-            }
         }
         st.to_ensure_var().reset();
     }
@@ -388,7 +390,6 @@ namespace arith {
         return true;
     }
 
-
     bool solver::internalize_term(expr* term) {
         if (!has_var(term))
             register_theory_var_in_lar_solver(internalize_def(term));
@@ -424,7 +425,7 @@ namespace arith {
         TRACE("arith", tout << mk_pp(t, m) << " " << force << " " << reflect(t) << "\n";);
         if (!force && !reflect(t))
             return;
-        for (expr* arg : *t)
+        for (expr* arg : *t) 
             e_internalize(arg);
     }