mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-03-27 13:35:40 +00:00
commit 1c5cf3638d
2 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/sls/sls_engine.cpp
View file

@ -868,6 +868,7 @@ bailout:
return res;
}
#if 0 // Old code.
// main search loop
lbool sls_engine::search_old() {
lbool res = l_undef;
@ -1060,6 +1061,7 @@ lbool sls_engine::search_old() {
}
}
}
#endif
bailout:
m_mpz_manager.del(new_value);
@ -1190,4 +1192,4 @@ unsigned sls_engine::check_restart(unsigned curr_value)
return 0;
}
return 1;
}
}

3
src/tactic/sls/sls_engine.h
View file

@ -114,7 +114,6 @@ public:
protected:
void checkpoint();
lbool search_old(void);
double get_restart_armin(unsigned cnt_restarts);
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
@ -148,4 +147,4 @@ protected:
inline unsigned check_restart(unsigned curr_value);
};
#endif
#endif