From 1706f77b9ec4bf7a333dd2b720f6a4d5db5c9d38 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Dec 2021 18:53:37 -0800
Subject: [PATCH] optimize propagation to only blocked literals

---
 src/sat/smt/euf_solver.cpp   | 2 +-
 src/sat/smt/smt_relevant.cpp | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index d8afa23ed..b8fbc5bd9 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -479,7 +479,7 @@ namespace euf {
             return sat::check_result::CR_CONTINUE;
 
         if (!init_relevancy())
-            give_up = true;
+            give_up = true;    
         
         unsigned num_nodes = m_egraph.num_nodes();
         auto apply_solver = [&](th_solver* e) {
diff --git a/src/sat/smt/smt_relevant.cpp b/src/sat/smt/smt_relevant.cpp
index 6a5da9df5..574ba0b42 100644
--- a/src/sat/smt/smt_relevant.cpp
+++ b/src/sat/smt/smt_relevant.cpp
@@ -215,6 +215,9 @@ namespace smt {
 
     void relevancy::propagate_relevant(sat::literal lit) {
         relevant_eh(lit);
+        euf::enode* n = ctx.bool_var2enode(lit.var());
+        if (n && !ctx.get_si().is_bool_op(n->get_expr()))
+            return;
         for (auto idx : occurs(~lit)) {
             if (m_roots[idx])
                 continue;