From acd48b6a301624789099a4fe0185f6fab99f5b72 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Tue, 11 Feb 2025 18:20:25 +0100
Subject: [PATCH] Fixing #7465 (#7551)

* Fixed bug in UP

* Put decrement at the right position

* Fixed replaying in UP

* Set UP persist clauses to false
---
 src/smt/params/smt_params_helper.pyg |  2 +-
 src/smt/smt_internalizer.cpp         |  7 +++++--
 src/smt/theory_user_propagator.cpp   | 14 ++++++--------
 3 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 23ea55af6..afea0e446 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -103,7 +103,7 @@ def_module_params(module_name='smt',
                           ('arith.print_ext_var_names', BOOL, False, 'print external variable names'),
                           ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
                           ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
-                          ('up.persist_clauses', BOOL, True, 'replay propagated clauses below the levels they are asserted'),
+                          ('up.persist_clauses', BOOL, False, 'replay propagated clauses below the levels they are asserted'),
                           ('array.weak', BOOL, False, 'weak array theory'),
                           ('array.extensional', BOOL, True, 'extensional array theory'),
                           ('clause_proof', BOOL, False, 'record a clausal proof'),
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 17c0033f0..5cfb4a8a8 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1142,10 +1142,13 @@ namespace smt {
         for (unsigned i = 0; i < num_lits; i++) {
             literal curr = lits[i];
             lbool   val  = get_assignment(curr);
-            switch(val) {
+            switch (val) {
             case l_false:
                 TRACE("simplify_aux_clause_literals", display_literal_verbose(tout << get_assign_level(curr) << " " << get_scope_level() << " " << curr << ":", curr); tout << "\n"; );
-                simp_lits.push_back(~curr);
+                if (curr != prev) {
+                    prev = curr;
+                    simp_lits.push_back(~curr);
+                }
                 break; // ignore literal                
                 // fall through
             case l_undef:
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index d3b312524..1079d43f6 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -339,22 +339,20 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) {
         ctx.mark_as_relevant(lit);
 
         m_lits.push_back(lit);
-        if (ctx.get_fparams().m_up_persist_clauses)
-            ctx.mk_th_axiom(get_id(), m_lits);
-        else
-            ctx.mk_th_lemma(get_id(), m_lits);
 
         if (ctx.get_fparams().m_up_persist_clauses) {
-            ctx.mk_th_axiom(get_id(), m_lits);
             expr_ref_vector clause(m);
-            for (auto lit : m_lits)
-                clause.push_back(ctx.literal2expr(lit));
+            for (auto l : m_lits)
+                clause.push_back(ctx.literal2expr(l));
             m_clauses_to_replay.push_back(clause);
-            if (m_replay_qhead + 1 < m_clauses_to_replay.size()) 
+            if (m_replay_qhead + 1 < m_clauses_to_replay.size())
                 std::swap(m_clauses_to_replay[m_replay_qhead], m_clauses_to_replay[m_clauses_to_replay.size()-1]);
             ctx.push_trail(value_trail<unsigned>(m_replay_qhead));
             ++m_replay_qhead;
+            ctx.mk_th_axiom(get_id(), m_lits);
         }
+        else
+            ctx.mk_th_lemma(get_id(), m_lits);
     }
     TRACE("user_propagate", ctx.display(tout););