From 98d3fabc24068182e1b321624a84e14a12db2fc0 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Mon, 10 Apr 2023 21:57:59 +0200
Subject: [PATCH] Bugfix relevancy propagation + UP (old core) (#6678)

* Some UP bugfixes in the new core

* Bugfix relevancy propagation + UP (old core)

* Revert smt_context.cpp
---
 src/smt/theory_user_propagator.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index f19f933f2ab..8eeaf4382da 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -92,6 +92,9 @@ void theory_user_propagator::propagate_cb(
 
     expr_ref _conseq(conseq, m);
     ctx.get_rewriter()(conseq, _conseq);
+    if (!ctx.get_manager().is_true(_conseq) && !ctx.get_manager().is_false(_conseq))
+        ctx.mark_as_relevant((expr*)_conseq);
+
     if (ctx.lit_internalized(_conseq) && ctx.get_assignment(ctx.get_literal(_conseq)) == l_true) 
         return;
     m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, _conseq));