From 0b8939d86e2d6ec67a3d1468fbca31503231fa95 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 16 Mar 2021 15:24:48 -0700
Subject: [PATCH] self-contained function for merge_tf

---
 src/ast/euf/euf_enode.h    | 1 +
 src/sat/smt/euf_solver.cpp | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h
index 2c67f66bc..fd9ef3d92 100644
--- a/src/ast/euf/euf_enode.h
+++ b/src/ast/euf/euf_enode.h
@@ -161,6 +161,7 @@ namespace euf {
         bool commutative() const { return m_commutative; }
         void mark_interpreted() { SASSERT(num_args() == 0); m_interpreted = true; }
         bool merge_enabled() const { return m_merge_enabled; }
+        bool merge_tf() const { return merge_enabled() && (class_size() > 1 || num_parents() > 0 || num_args() > 0); }
 
         enode* get_arg(unsigned i) const { SASSERT(i < num_args()); return m_args[i]; }        
         unsigned hash() const { return m_expr->hash(); }
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 710e98408..6155f6b20 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -308,7 +308,7 @@ namespace euf {
             euf::enode* nb = n->get_arg(1);
             m_egraph.merge(na, nb, c);
         }
-        else if (n->merge_enabled() && (n->num_parents() > 0 || n->num_args() > 0)) {
+        else if (n->merge_tf()) {
             euf::enode* nb = sign ? mk_false() : mk_true();
             m_egraph.merge(n, nb, c);
         }