mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

fix default parameter regression

Browse source 
bug introduced in commit 63f48f8fd4
This commit is contained in:
Nuno Lopes 2022-08-23 15:26:29 +01:00
parent 7ab904bfc6
commit 916d1dbb13
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/params/smt_params.h
View file

@ -91,9 +91,9 @@ struct smt_params : public preprocessor_params,
unsigned m_relevancy_lvl = 2;
bool m_relevancy_lemma = false;
unsigned m_random_seed = 0;
double m_random_var_freq = 1.052;
double m_inv_decay = 1;
unsigned m_clause_decay;
double m_random_var_freq = 0.01;
double m_inv_decay = 1.052;
unsigned m_clause_decay = 1;
initial_activity m_random_initial_activity = initial_activity::IA_RANDOM_WHEN_SEARCHING;
phase_selection m_phase_selection = phase_selection::PS_CACHING_CONSERVATIVE;
unsigned m_phase_caching_on = 700;