include "Clight/test/null-op.c.ma".

example exec: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 50 [ ]).
normalize  (* you can examine the result here *)
@refl
qed.