mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

bypass replaying new clause within propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-02-04 15:26:17 -08:00
parent 3b90816025
commit 3cec3fc63d
1 changed files with 3 additions and 0 deletions

3
src/smt/theory_user_propagator.cpp
View file

@ -345,6 +345,9 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) {
for (auto lit : m_lits)
clause.push_back(ctx.literal2expr(lit));
m_clauses_to_replay.push_back(clause);
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]);
++m_replay_qhead;
}
else {
ctx.mk_th_lemma(get_id(), m_lits);