mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 04:03:39 +00:00
add back use of all variables for tracking
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
cec6ced457
commit
561a4331a8
|
@ -257,6 +257,7 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
|
||||||
vars.push_back(i);
|
vars.push_back(i);
|
||||||
g_solver->set_external(i);
|
g_solver->set_external(i);
|
||||||
}
|
}
|
||||||
|
num_vars = g_solver->num_vars();
|
||||||
lbool r;
|
lbool r;
|
||||||
if (use_chunk) {
|
if (use_chunk) {
|
||||||
r = core_chunking(*g_solver, vars, assumptions, conseq, 100);
|
r = core_chunking(*g_solver, vars, assumptions, conseq, 100);
|
||||||
|
|
Loading…
Reference in a new issue