diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 845ac645c..968dcacd8 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -2107,6 +2107,21 @@ void cmd_context::analyze_failure(expr_mark& seen, model_evaluator& ev, expr* a,
                << (expected_value?"true":"false") << "\n";);                
 
     IF_VERBOSE(11, display_detailed_analysis(verbose_stream(), ev, a));
+
+    if (m().is_iff(a)) {
+        ptr_vector<expr> todo;
+        todo.push_back(a);
+        for (unsigned i = 0; i < todo.size(); ++i) {
+            e = todo[i];
+            if (m().is_and(e) || m().is_or(e) || m().is_iff(e) || m().is_implies(e) || m().is_not(e)) 
+                for (expr* arg : *to_app(e))
+                    todo.push_back(arg);
+            else
+                IF_VERBOSE(10, verbose_stream() << "#" << e->get_id() << " " << mk_bounded_pp(e, m()) << " " << (ev.is_true(e)?"true":"false") << "\n");
+        }
+        return;
+    }
+
 }
 
 void cmd_context::display_detailed_analysis(std::ostream& out, model_evaluator& ev, expr* e) {
diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index 66ed9054c..73fe49506 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -73,6 +73,7 @@ namespace euf {
         if (!m_enabled)
             return;
         flush();
+        TRACE("relevancy", tout << "root " << sat::literal_vector(n, lits) << "\n");
         sat::literal true_lit = sat::null_literal;
         for (unsigned i = 0; i < n; ++i) {
             if (ctx.s().value(lits[i]) == l_true) {
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 7c8a42bf1..bb2d61b0a 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -806,6 +806,8 @@ namespace euf {
     }
 
     bool solver::set_root(literal l, literal r) {
+        if (m_relevancy.enabled())
+            return false;
         expr* e = bool_var2expr(l.var());
         if (!e)
             return true;
diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp
index 9ad2a17ed..4b787561d 100644
--- a/src/smt/smt_relevancy.cpp
+++ b/src/smt/smt_relevancy.cpp
@@ -134,11 +134,11 @@ namespace smt {
         obj_map<expr, relevancy_ehs *> m_relevant_ehs;
         obj_map<expr, relevancy_ehs *> m_watches[2];
         struct eh_trail {
-            enum kind { POS_WATCH, NEG_WATCH, HANDLER };
+            enum class kind { POS_WATCH, NEG_WATCH, HANDLER };
             kind   m_kind;
             expr * m_node;
-            eh_trail(expr * n):m_kind(HANDLER), m_node(n) {}
-            eh_trail(expr * n, bool val):m_kind(val ? POS_WATCH : NEG_WATCH), m_node(n) {}
+            eh_trail(expr * n):m_kind(kind::HANDLER), m_node(n) {}
+            eh_trail(expr * n, bool val):m_kind(val ? kind::POS_WATCH : kind::NEG_WATCH), m_node(n) {}
             kind get_kind() const { return m_kind; }
             expr * get_node() const { return m_node; }
         };
@@ -292,9 +292,9 @@ namespace smt {
                 expr * n = t.get_node();
                 relevancy_ehs * ehs;
                 switch (t.get_kind()) {
-                case eh_trail::POS_WATCH: ehs = get_watches(n, true); SASSERT(ehs); set_watches(n, true, ehs->tail()); break;
-                case eh_trail::NEG_WATCH: ehs = get_watches(n, false); SASSERT(ehs); set_watches(n, false, ehs->tail()); break;
-                case eh_trail::HANDLER:   ehs = get_handlers(n); SASSERT(ehs); set_handlers(n, ehs->tail()); break;
+                case eh_trail::kind::POS_WATCH: ehs = get_watches(n, true); SASSERT(ehs); set_watches(n, true, ehs->tail()); break;
+                case eh_trail::kind::NEG_WATCH: ehs = get_watches(n, false); SASSERT(ehs); set_watches(n, false, ehs->tail()); break;
+                case eh_trail::kind::HANDLER:   ehs = get_handlers(n); SASSERT(ehs); set_handlers(n, ehs->tail()); break;
                 default: UNREACHABLE(); break;
                 }
                 m.dec_ref(n);