8497bafa2e
- Translation to z3z now evaluates constant expressions instead of abstracting them. This non-feature could cause "false" synthesis failures due to non-translatable yet constant expressions possibly introduced by tomato (or manually), for instance `not false' in node `n' bellow: node n (a: bool) returns (ok: bool) contract assume true enforce ok with () let ok = a or not false; tel |
||
---|---|---|
.. | ||
sigali.ml | ||
sigali.mli | ||
sigalimain.ml | ||
sigalimain.mli |