From b658934bd8bd87f8e6dc9c117d9fda061dad2fd9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Apr 2021 10:16:44 -0700
Subject: [PATCH] fix #5197 fix #5193

---
 src/smt/theory_seq.cpp | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 6c5612c37..89f224e2e 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1872,11 +1872,14 @@ public:
 
 app* theory_seq::get_ite_value(expr* e) {
     expr* e1, *e2, *e3;
-    while (m.is_ite(e, e1, e2, e3)) {
-        if (get_root(e2) == get_root(e)) {
+    while (m.is_ite(e, e1, e2, e3)) {        
+        if (!ctx.e_internalized(e))
+            break;
+        enode* r = ctx.get_enode(e)->get_root();
+        if (ctx.get_enode(e2)->get_root() == r) {
             e = e2;
         }
-        else if (get_root(e3) == get_root(e)) {
+        else if (ctx.get_enode(e3)->get_root() == r) {
             e = e3;
         }
         else {