From f87e187b629891cf1ec3e6e43d29f87457520c63 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 23 Nov 2022 17:52:14 +0700
Subject: [PATCH] #6429

---
 src/ast/euf/euf_egraph.cpp | 7 ++++---
 src/sat/smt/euf_model.cpp  | 2 ++
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 1448ee8d7..037020a2e 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -158,6 +158,8 @@ namespace euf {
     }
 
     void egraph::add_literal(enode* n, enode* ante) {
+        if (n->bool_var() == sat::null_bool_var)
+            return;
         TRACE("euf_verbose", tout << "lit: " << n->get_expr_id() << "\n";);
         m_new_lits.push_back(enode_pair(n, ante));
         m_updates.push_back(update_record(update_record::new_lit()));
@@ -272,9 +274,8 @@ namespace euf {
             if (enable_merge_tf && n->value() != l_undef && !m.is_value(n->get_root()->get_expr())) {
                 expr* b = n->value() == l_true ? m.mk_true() : m.mk_false();
                 enode* tf = find(b);
-                if (!tf) 
-                    tf = mk(b, 0, 0, nullptr);
-                add_literal(n, tf);
+                if (tf) 
+                    add_literal(n, tf);
             }
         }
     }
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index eef873afa..0fd021d70 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -348,6 +348,8 @@ namespace euf {
                 continue;
             if (!is_relevant(n))
                 continue;
+            if (n->bool_var() == sat::null_bool_var)
+                continue;
             bool tt = l_true == s().value(n->bool_var());
             if (tt && !mdl.is_false(e))
                 continue;