Revision 503d035509bd518c18a45b04244b317c75204d7e authored by Pierre Boutry on 19 March 2024, 10:29:37 UTC, committed by Pierre-Yves Strub on 05 April 2024, 18:16:56 UTC
1 parent 30bfa95
procchange.ec
require import AllCore.
module M = {
proc f(x : int) = {
x <- x + 0;
}
}.
lemma L : equiv[M.f ~ M.f : true ==> true].
proof.
proc.
proc change {1} 1 : x.
- smt().
abort.
Computing file changes ...
