mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-21 04:58:00 -07:00
parent 959f150e4a
commit 23963f274d
1 changed files with 5 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -532,18 +532,13 @@ namespace polysat {
case l_true:
return;
case l_false:
continue;
default:
if (lit2cnstr(lit).is_currently_false(*this)) {
num_choices++;
continue;
}
break;
case l_undef:
num_choices++;
if (!lit2cnstr(lit).is_currently_false(*this))
choice = lit;
break;
}
num_choices++;
if (choice == sat::null_literal)
choice = lit;
}
LOG_V("num_choices: " << num_choices);
if (choice == sat::null_literal) {