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

with bounded

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-01 04:58:38 -07:00
parent fa9cf0fa0c
commit 03e92f3f20
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_solver.cpp
View file

@ -1602,7 +1602,7 @@ namespace sat {
} }
lbool solver::bounded_search() { lbool solver::bounded_search() {
#if 0 #if 1
lbool is_sat = l_undef; lbool is_sat = l_undef;
while (is_sat == l_undef && !should_cancel()) { while (is_sat == l_undef && !should_cancel()) {
if (inconsistent()) is_sat = resolve_conflict_core(); if (inconsistent()) is_sat = resolve_conflict_core();