From 5ed27a6c3876e83522ff85769d4b1fc1e65e86ba Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Dec 2021 12:06:56 -0800
Subject: [PATCH] fix initialization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/euf_solver.cpp   | 2 ++
 src/sat/smt/smt_relevant.cpp | 4 +++-
 src/sat/smt/smt_relevant.h   | 1 +
 3 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index ca931ce8f..d6ba945db 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -52,6 +52,7 @@ namespace euf {
         m_values(m)
     {
         updt_params(p);
+        m_relevancy.set_enabled(get_config().m_relevancy_lvl > 2);
 
         std::function<void(std::ostream&, void*)> disp =
             [&](std::ostream& out, void* j) { 
@@ -70,6 +71,7 @@ namespace euf {
 
     void solver::updt_params(params_ref const& p) {
         m_config.updt_params(p);
+        std::cout << get_config().m_relevancy_lvl << "\n";
     }
 
     /**
diff --git a/src/sat/smt/smt_relevant.cpp b/src/sat/smt/smt_relevant.cpp
index 9d118001c..b88f204cb 100644
--- a/src/sat/smt/smt_relevant.cpp
+++ b/src/sat/smt/smt_relevant.cpp
@@ -22,7 +22,6 @@ Author:
 namespace smt {
 
     relevancy::relevancy(euf::solver& ctx): ctx(ctx) {
-        m_enabled = ctx.get_config().m_relevancy_lvl > 2;
     }
 
     void relevancy::relevant_eh(euf::enode* n) {
@@ -73,6 +72,9 @@ namespace smt {
             case update::set_root:
                 m_roots[idx] = false;
                 break;
+            case update::set_qhead:
+                m_qhead = idx;
+                break;
             default:
                 UNREACHABLE();
                 break;
diff --git a/src/sat/smt/smt_relevant.h b/src/sat/smt/smt_relevant.h
index a20ca1b44..902a005f4 100644
--- a/src/sat/smt/smt_relevant.h
+++ b/src/sat/smt/smt_relevant.h
@@ -143,6 +143,7 @@ namespace smt {
         bool is_relevant(expr* e) const { return !m_enabled || m_relevant_expr_ids.get(e->get_id(), false); }
         
         bool enabled() const { return m_enabled; }
+        void set_enabled(bool e) { m_enabled = e; }
 
         void add_relevant(euf::th_solver* th) { m_relevant_eh.push_back(th); }
     };