kind2-mc/kind2 — pull request #203 by AdrienChampion (2014-12-22 17:43:25+00:00)
Title: Fixed svar unrolling, invGen uses 3 solvers now.

### State var unrolling ###

State var unrolling has changed to support multi solver. As a result, solvers should be initialized using TransSys.init_define_fun_declare_vars_of_bounds which defines functions and declares vars.
Do not forget to declare variables at -1 for two state invariant generation.

Initialization in step for instance:
```ocaml
TransSys.init_define_fun_declare_vars_of_bounds
trans
(Solver.define_fun solver)
(Solver.declare_fun solver)
Numeral.(~- one) Numeral.one
```
Unrolling to the next k in step:
```ocaml
TransSys.declare_vars_of_bounds
trans (Solver.declare_fun solver) k_p_1 k_p_1 ;
TransSys.trans_of_bound trans k_p_1
|> Solver.assert_term solver ;
```

### Invariant generation ###
Invariant generation new uses three solvers:
* one for base,
* one for step,
* one for trivial candidate invariant pruning.