diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 9b79fbfe33..191afdeac6 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1734,14 +1734,12 @@ namespace smt {
         void internalize_instance(expr * body, proof * pr, unsigned generation) {
             internalize_assertion(body, pr, generation);
             if (relevancy()) {
-                if (inconsistent()) {
-                    app * a = to_app(body);
-                    SASSERT(a->get_decl_kind() == OP_OR);
-                    SASSERT(to_app(a->get_arg(0))->get_decl_kind() == OP_NOT);
-                    SASSERT(is_quantifier(to_app(a->get_arg(0))->get_arg(0)));
-                    for (unsigned i = 1; i < a->get_num_args(); ++i) {
-                        mark_as_relevant(a->get_arg(i));
-                    }
+                // 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() && is_app(body)) {
+                    for (auto arg : *to_app(body))
+                        mark_as_relevant(arg);
                 }
                 m_case_split_queue->internalize_instance_eh(body, generation);
             }