- fix simplifier.ml
- refactor auxiliary precondition generation for tail-rec procedures