Seg fault in rewrite

[mbbarbosa]

The following proof causes a seg fault.

require import AllCore IntDiv List.
from Jasmin require import JModel.

lemma SAR_sem10 (a : W16.t) : a |>> W8.of_int 10 = W16.of_int (to_sint a %/ 2^10).
+ have H : all (fun i => let a = W16.of_int i in
                                     a |>> W8.of_int 10 = W16.of_int (to_sint a %/ 2^10)) (iota_ 0 W16.modulus); last first.
   rewrite allP in H => /=; move : (H (to_uint a)) => /=.
   rewrite mem_iota /=;have := (W16.to_uint_cmp a) => /= /#.
rewrite -iotaredE /=.

[fdupress]

Can't look now, but will likely need some detail from opam list to reproduce (compiler version, in particular).

And the Jasmin eclib version/commit hash as well, just to make sure we cover everything.

[mbbarbosa]

ocaml 4.14.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.1 Official release 4.14.1

Jasmin commit: 470ac5f6f923efffbc0021edf718aa30a2d0f0db

[strub]

This is the reduction of iotared that is causing a stack overflow. The reduction engine is not tail-call.

[strub]

Superseded by #629