diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 9664dd73e..0248c75a6 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1786,8 +1786,8 @@ namespace smt {
                 // if the instantiation creates a conflict, we backtrack immediately.
                 // to retain the conflict clause being relevant we mark it here.
                 // if the instantiation does not create a conflict, default relevancy propagation applies.
-                if (inconsistent()) 
-                    mark_as_relevant(body);
+                //if (inconsistent() && is_app(body)) 
+                //    for (auto arg: *to_app(body)) mark_as_relevant(arg);
                 
                 m_case_split_queue->internalize_instance_eh(body, generation);
             }