diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index 6b61bec62..b54e92a70 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -385,10 +385,10 @@ namespace smt {
                 expr* e = kv.m_key;
                 expr* val = kv.m_value;
                 literal lit = mk_diseq(e, val);
-                mark_as_relevant(lit);
                 if (get_assignment(lit) != l_undef) {
                     continue;
                 }
+                mark_as_relevant(lit);
                 ++num_vars;
                 push_scope();
                 assign(lit, b_justification::mk_axiom(), true);
diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp
index 5bc7bf9d2..6d20072cb 100644
--- a/src/smt/smt_relevancy.cpp
+++ b/src/smt/smt_relevancy.cpp
@@ -333,7 +333,8 @@ namespace smt {
                 if (e != nullptr) {
                     enode * curr = e;
                     do {
-                        set_relevant(curr->get_expr());
+                        if (!is_relevant_core(curr->get_expr()))
+                            set_relevant(curr->get_expr());
                         curr = curr->get_next();
                     }
                     while (curr != e);