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

bvsls refactoring

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-03-28 14:58:59 +00:00
parent 8e5659ac4c
commit 24d662ba49
2 changed files with 14 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -109,6 +109,8 @@ public:
void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted);
void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped);
void init_tracker(void);
lbool search(void);
void operator()(goal_ref const & g, model_converter_ref & mc);