mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Comment on params used in spacer_context

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-22 14:48:11 -07:00
parent 55126692c9
commit 40781c0b0c
1 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2301,16 +2301,15 @@ void context::init_global_smt_params() {
fparams.m_mbqi = m_params.spacer_mbqi();
if (!m_params.spacer_ground_cti()) {
fparams.m_pi_use_database = true;
fparams.m_pi_use_database = true; // you don't need this
fparams.m_phase_selection = PS_CACHING_CONSERVATIVE2;
fparams.m_restart_strategy = RS_GEOMETRIC;
fparams.m_restart_factor = 1.5;
fparams.m_eliminate_bounds = true;
fparams.m_qi_quick_checker = MC_UNSAT;
fparams.m_propagate_booleans = true;
fparams.m_qi_quick_checker = MC_UNSAT; //
fparams.m_qi_eager_threshold = 10;
fparams.m_qi_lazy_threshold = 20;
fparams.m_ng_lift_ite = LI_FULL;
fparams.m_ng_lift_ite = LI_FULL; // ? probably useless
}
}