3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00

revert to native chunker

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-01 15:22:52 -07:00
parent d14f2af5ae
commit f9105edb14

View file

@ -3259,9 +3259,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
}
}
is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100);
// is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100);
// is_sat = get_consequences(asms, lits, conseq);
is_sat = get_consequences(asms, lits, conseq);
set_model(mdl);
return is_sat;
}