mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

Removed unused options

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-31 15:18:36 -07:00
parent 0b387cd7eb
commit ada548b5ae
2 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/base/fixedpoint_params.pyg
View file

@ -153,7 +153,6 @@ def_module_params('fixedpoint',
('spacer.eager_reach_check', BOOL, True, 'SPACER: eagerly check if a query is reachable using reachability facts of predecessors'),
('spacer.use_lemma_as_cti', BOOL, False, 'SPACER: use a lemma instead of a CTI in flexible_trace'),
('spacer.reset_obligation_queue', BOOL, True, 'SPACER: reset obligation queue when entering a new level'),
('spacer.init_reach_facts', BOOL, True, 'SPACER: initialize reachability facts with false'),
('spacer.use_array_eq_generalizer', BOOL, True, 'SPACER: attempt to generalize lemmas with array equalities'),
('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'),
('xform.array_blast', BOOL, False, "try to eliminate local array terms using Ackermannization -- some array terms may remain"),
@ -161,7 +160,6 @@ def_module_params('fixedpoint',
('spacer.skip_propagate', BOOL, False, "Skip propagate/pushing phase. Turns PDR into a BMC that returns either reachable or unknown"),
('spacer.max_level', UINT, UINT_MAX, "Maximum level to explore"),
('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),
('spacer.reach_as_init', BOOL, True, "Extend initial rules with computed reachability facts"),
('spacer.blast_term_ite', BOOL, True, "Expand non-Boolean ite-terms"),
('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministically"),
('spacer.reach_dnf', BOOL, True, "Restrict reachability facts to DNF"),

4
src/muz/spacer/spacer_context.cpp
View file

@ -1019,7 +1019,7 @@ void pred_transformer::add_reach_fact (reach_fact *fact)
expr_ref fml (m);
if (!m_reach_case_vars.empty()) {last_var = m_reach_case_vars.back();}
if (fact->is_init () || !ctx.get_params ().spacer_reach_as_init ())
if (fact->is_init ())
{new_var = mk_fresh_reach_case_var();}
else {
new_var = extend_initial (fact->get ())->get_arg (0);
@ -1308,7 +1308,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
expr_ref a(m);
pm.formula_n2o(pt.get_last_reach_case_var (), a, i);
reach_assumps.push_back(m.mk_not (a));
} else if (ctx.get_params().spacer_init_reach_facts()) {
} else {
reach_assumps.push_back(m.mk_not (entry.m_key));
break;
}