From 41e11857e505ca27e77f15659dba0ed5440d5ed0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Apr 2020 10:57:49 -0700
Subject: [PATCH] fix #3744

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ebb6e8c48..4ed428d02 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -587,7 +587,7 @@ class theory_lra::imp {
                 terms[index] = n1;
                 if (!ctx().e_internalized(n)) {
                     app* t = to_app(n);
-                    internalize_args(t);
+                    VERIFY(internalize_term(to_app(n1)));
                     mk_enode(t);
                     theory_var v = mk_var(n);
                     theory_var w = mk_var(n1);