mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

SLS tactic: compilation fixes

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-06-03 18:17:41 +01:00
parent 56bfc06c4f
commit 7c32df93a4
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/sls/sls_tactic.cpp
View file

@ -1370,7 +1370,7 @@ class sls_tactic : public tactic {
void updt_params(params_ref const & p) { void updt_params(params_ref const & p) {
m_produce_models = p.get_bool("produce_models", false); m_produce_models = p.get_bool("produce_models", false);
m_max_restarts = p.get_uint("sls_restarts", -1); m_max_restarts = p.get_uint("sls_restarts", (unsigned)-1);
m_tracker.set_random_seed(p.get_uint("random_seed", 0)); m_tracker.set_random_seed(p.get_uint("random_seed", 0));
m_plateau_limit = p.get_uint("plateau_limit", 100); m_plateau_limit = p.get_uint("plateau_limit", 100);
} }
@ -1612,7 +1612,7 @@ class sls_tactic : public tactic {
lbool search(goal_ref const & g) { lbool search(goal_ref const & g) {
lbool res = l_undef; lbool res = l_undef;
double score = 0.0, old_score = 0.0; double score = 0.0, old_score = 0.0;
unsigned new_const = -1, new_bit = 0; unsigned new_const = (unsigned)-1, new_bit = 0;
mpz new_value; mpz new_value;
move_type move; move_type move;
@ -1631,7 +1631,7 @@ class sls_tactic : public tactic {
checkpoint(); checkpoint();
old_score = score; old_score = score;
new_const = -1; new_const = (unsigned)-1;
ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(g); ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(g);