From b4873d226c0d093577b9f4181f9c6d9ed8f51cdf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 20 Mar 2022 11:40:19 -0700
Subject: [PATCH] fix #5907

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_datatype.cpp | 2 ++
 1 file changed, 2 insertions(+)

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);