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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-05 10:36:24 +01:00
parent 8b0d540cca
commit 7d73069798
1 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_unit_walk.cpp
View file

@ -105,7 +105,6 @@ namespace sat {
init_phase(); init_phase();
lbool st = l_undef; lbool st = l_undef;
while (s.rlimit().inc() && st == l_undef) { while (s.rlimit().inc() && st == l_undef) {
std::cout << "walk " << st << "\n";
if (inconsistent() && !m_decisions.empty()) do_pop(); if (inconsistent() && !m_decisions.empty()) do_pop();
else if (inconsistent()) st = l_false; else if (inconsistent()) st = l_false;
else if (should_restart()) restart(); else if (should_restart()) restart();
@ -145,7 +144,6 @@ namespace sat {
lbool unit_walk::do_backjump() { lbool unit_walk::do_backjump() {
unsigned backjump_level = m_decisions.size(); // - (m_decisions.size()/20); unsigned backjump_level = m_decisions.size(); // - (m_decisions.size()/20);
lbool st = update_priority(backjump_level); lbool st = update_priority(backjump_level);
std::cout << "update " << st << "\n";
switch (st) { switch (st) {
case l_true: return l_true; case l_true: return l_true;
case l_false: break; // TBD case l_false: break; // TBD