Mohamed Iguernlala

fixes https://github.com/OCamlPro/liquidity/issues/261

``` [%%entry let play (var23 : int) (storage : storage) = (let some60 = Some ((Current.sender ()), var23) in let storage_fst61 = storage.(0p) in let res62 = match storage_fst61 with...

[IntervalCalculus] Assertion failed, line 231

1

Commit ID: ac84c736c27b1f1d3ede360d0a36e9b40d8899b2 File: AE-format/why3-no-split/binary_multiplication-BinaryMultiplication63-VC_binary_mult.ae.zip Reason: case-split for an integer expression extracted from the simplex is a non-integer constant, although it's equal to min/max bound.

On timeout, SAT solvers (probably) return `Unknown {env; timeout_reason}`, where `timeout_reason` is one of {Assume, ProofSearch, ModelGen} ``` type timeout_reason = | NoTimeout | Assume | ProofSearch | ModelGen ```...

The following formula is unsat: ``` (declare-fun s () Int) (declare-fun y () Int) (declare-fun th () Int) (assert (> s 0)) (assert (>= s (+ (* y s) 1)))...

See what has been done for Arithmetic's `add` here: https://github.com/OCamlPro/alt-ergo/pull/432/commits/c02878cb2758ae96a28e52a4fae6f1461ae1b15d

Currently, a let symbol is seen as a Var, and eliminated by introduction a skolem-like function.