From 3e84d04719976ae51c8fe20b14e1a67bf8958536 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 12 Mar 2020 19:47:26 -0700
Subject: [PATCH] fix internalize for multiplication #3119

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 31 ++++++++++---------------------
 1 file changed, 10 insertions(+), 21 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index b613cce6a..85289f81b 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -670,36 +670,25 @@ class theory_lra::imp {
 
     void internalize_mul(app* t, theory_var& v, rational& r) {
         SASSERT(a.is_mul(t));
+        internalize_args(t);
         bool _has_var = has_var(t);
-        if (!_has_var) {
-            internalize_args(t);
-            mk_enode(t);
-        }
-        r = rational::one();
-        rational r1;
+        mk_enode(t);
         v = mk_var(t);
         svector<lpvar> vars;
-        ptr_buffer<expr> todo;
-        todo.push_back(t);
-        while (!todo.empty()) {
-            expr* n = todo.back();
-            todo.pop_back();
-            if (a.is_mul(n)) {
-                for (expr* arg : *to_app(n)) {
-                    todo.push_back(arg);
-                }
-            }
-            else if (a.is_numeral(n, r1)) {
+        r = rational::one();
+        rational r1;
+
+        for (expr* n : *t) {
+            if (a.is_numeral(n, r1)) {
                 r *= r1;
             }
             else {
-                if (!ctx().e_internalized(n)) {
-                    ctx().internalize(n, false);
-                }
+                SASSERT(ctx().e_internalized(n));
                 vars.push_back(register_theory_var_in_lar_solver(mk_var(n)));
             }
         }
-        TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << " " << _has_var << "\n";);
+
+        TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n";);
         if (!_has_var) {
             if (m_solver->m_need_register_terms == false) {
                 m_solver->m_need_register_terms = true;