mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Update viable2.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-11-16 09:54:06 -08:00
parent 69a17d0c60
commit a5fdf6ba8a
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/polysat/viable2.cpp
View file

@ -72,6 +72,11 @@ namespace polysat {
if (e && e->interval.is_full()) if (e && e->interval.is_full())
return; return;
if (ne->interval.is_currently_empty()) {
m_alloc.push_back(ne);
return;
}
auto create_entry = [&]() { auto create_entry = [&]() {
m_trail.push_back({ v, ne }); m_trail.push_back({ v, ne });
s.m_trail.push_back(trail_instr_t::viable_add_i); s.m_trail.push_back(trail_instr_t::viable_add_i);