From ae6aea7a4d8309710eeafcf3b5c67e4be6086bbe Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Jun 2021 13:48:51 -0700
Subject: [PATCH] #5324

---
 src/sat/smt/euf_internalize.cpp |  4 ++--
 src/sat/smt/euf_solver.h        |  5 ++++-
 src/sat/smt/q_solver.cpp        | 10 ++++++++--
 3 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index 2c01118c9..d3a95c689 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -193,8 +193,8 @@ namespace euf {
             }
             s().mk_clause(lits, st);
             if (relevancy_enabled())
-                add_root(lits.size(), lits.data());
-    }
+                add_root(lits);
+        }
         else {
             // g(f(x_i)) = x_i
             // f(x_1) = a + .... + f(x_n) = a >= 2
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index ae9ba1488..b0bfcd4ff 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -357,8 +357,11 @@ namespace euf {
         // relevancy
         bool relevancy_enabled() const { return get_config().m_relevancy_lvl > 0; }
         void add_root(unsigned n, sat::literal const* lits);
+        void add_root(sat::literal_vector const& lits) { add_root(lits.size(), lits.data()); }
+        void add_root(sat::literal lit) { add_root(1, &lit); }
+        void add_root(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_root(2, lits); }
         void add_aux(unsigned n, sat::literal const* lits);
-        void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); }
+        void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } 
         void track_relevancy(sat::bool_var v);
         bool is_relevant(expr* e) const;
         bool is_relevant(enode* n) const;
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 2035cd533..66f1323cf 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -42,8 +42,12 @@ namespace q {
 
         auto const& exp = expand(q);
         if (exp.size() > 1 && is_forall(q)) {
-            for (expr* e : exp) 
-                add_clause(~l, ctx.internalize(e, l.sign(), false, false));                    
+            for (expr* e : exp) {
+                sat::literal lit = ctx.internalize(e, l.sign(), false, false); 
+                add_clause(~l, lit);                    
+                if (ctx.relevancy_enabled())
+                    ctx.add_root(~l, lit);
+            }
             return;
         }
         if (exp.size() > 1 && is_exists(q)) {
@@ -52,6 +56,8 @@ namespace q {
             for (expr* e : exp)
                 lits.push_back(ctx.internalize(e, l.sign(), false, false));
             add_clause(lits);
+            if (ctx.relevancy_enabled())
+                ctx.add_root(lits);
             return;
         }