diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 1aa8bbea3..035b647dc 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -254,6 +254,8 @@ namespace smt {
         app_ref n_is_con(m.mk_app(rec, own), m);
         ctx.internalize(n_is_con, false);
         literal lits[2] = { ~is_con, literal(ctx.get_bool_var(n_is_con)) };
+        ctx.mark_as_relevant(lits[0]);
+        ctx.mark_as_relevant(lits[1]);
         std::function<literal_vector(void)> fn = [&]() { return literal_vector(2, lits); };
         scoped_trace_stream _st(*this, fn);
         ctx.mk_th_axiom(get_id(), 2, lits);