From ab34ef9daffe62c741217c548f629fa1c0b901e5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 25 Mar 2020 01:57:05 -0700
Subject: [PATCH] fix crash exposed by #3503

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

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index a27174841..bed099345 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -675,8 +675,8 @@ class theory_lra::imp {
         
     }
 
-    void internalize_args(app* t) {
-        if (!reflect(t)) 
+    void internalize_args(app* t, bool force = false) {
+        if (!force && !reflect(t)) 
             return;
         for (expr* arg : *t) {
             if (!ctx().e_internalized(arg)) {
@@ -687,7 +687,7 @@ class theory_lra::imp {
 
     theory_var internalize_mul(app* t) {
         SASSERT(a.is_mul(t));
-        internalize_args(t);
+        internalize_args(t, true);
         bool _has_var = has_var(t);
         mk_enode(t);
         theory_var v = mk_var(t);