include "common/Animation.ma".
include "Clight/test/castremoval.c.ma".

example exec: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
normalize  (* you can examine the result here *)
%
qed.

include "Clight/SimplifyCasts.ma".

example simplified: result ? (simplify_program myprog).
normalize
%
qed.

example exec_s: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [EVint I32 (repr I32 0)]).
normalize  (* you can examine the result here *)
%
qed.