From 614c66f1e2c44509fa068a9387df370b2b4deeaf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 3 Jan 2022 17:21:37 -0800
Subject: [PATCH] missing relevancy propagation

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

diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index d42a5a353..8a7d16b31 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -304,6 +304,8 @@ namespace euf {
                 literal lits2[2] = { lit_c, lit_el };
                 s().add_clause(2, lits1, st);
                 s().add_clause(2, lits2, st);
+                add_root(2, lits1);
+                add_root(2, lits2);
             }
         }
         else if (m.is_distinct(e)) {
@@ -322,6 +324,8 @@ namespace euf {
             sat::literal lits2[2] = { dist, some_eq };
             s().add_clause(2, lits1, st);
             s().add_clause(2, lits2, st);
+            add_root(2, lits1);
+            add_root(2, lits2);
         }
         else if (m.is_eq(e, th, el) && !m.is_iff(e)) {
             sat::literal lit1 = expr2literal(e);
@@ -334,6 +338,8 @@ namespace euf {
                 sat::literal lits2[2] = { lit1, ~lit2 };
                 s().add_clause(2, lits1, st);
                 s().add_clause(2, lits2, st);
+                add_root(2, lits1);
+                add_root(2, lits2);
             }
         }
     }