mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

we have to replay in order, otherwise dependencies could become shuffled

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-08 00:06:22 +02:00
parent efdab0cd4c
commit 8bcec83ee8
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/solver.cpp
View file

@ -308,7 +308,8 @@ namespace polysat {
pop_constraints(m_redundant);
m_constraints.release_level(m_level + 1);
SASSERT(m_level == target_level);
for (auto c : replay) {
for (unsigned j = replay.size(); j-- > 0; ) {
auto c = replay[j];
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(c.blit());
c.narrow(*this);