From 9aad331699b472c100ace108ebc248e2bb816572 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 14 Sep 2021 10:32:53 +0200
Subject: [PATCH] #5546

try dampening
---
 src/smt/user_propagator.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp
index 1bbb6073a..7fbfd567f 100644
--- a/src/smt/user_propagator.cpp
+++ b/src/smt/user_propagator.cpp
@@ -52,6 +52,8 @@ void user_propagator::propagate_cb(
     unsigned num_fixed, unsigned const* fixed_ids, 
     unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, 
     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, expr_ref(conseq, m)));
 }