From a6dce246f6d6cb79439ea20a0049d44041834a3f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 15 Feb 2021 14:36:01 -0800
Subject: [PATCH] fix #5031

---
 src/smt/theory_lra.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 4eeba4e9d..b42b9a699 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -550,6 +550,9 @@ class theory_lra::imp {
             return get_enode(n);
         }
         else {
+            if (reflect(n))
+                for (expr* arg : *n)
+                    th.ensure_enode(arg);
             return ctx().mk_enode(n, !reflect(n), false, enable_cgc_for(n));       
         }
     }