From 4da4591fe73c7541156760862c655b386e2d9364 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Apr 2021 15:40:17 -0700
Subject: [PATCH] #5215

---
 src/sat/smt/euf_model.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index a9a721ccc..2e9d155a9 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -144,6 +144,16 @@ namespace euf {
                     m_values.set(id, m.mk_false());
                     continue;
                 }
+                switch (n->value()) {
+                case l_true:
+                    m_values.set(id, m.mk_true());
+                    continue;
+                case l_false:
+                    m_values.set(id, m.mk_false());
+                    continue;
+                default:
+                    break;
+                }
                 if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id())
                     continue;
                 sat::bool_var v = get_enode(e)->bool_var();