blob: 0bb87c65480963b1949ea080e9d469d605ef0bb8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Require Import Int63 Cyclic63.
Open Scope int63_scope.
(* This used to go through because of an unbalanced stack bug in the bytecode
interpreter *)
Lemma bad : False.
assert (1 = 2).
change 1 with (Int63.add (Int63.addmuldiv 129 (Int63.add 1 1) 2) 1).
Fail vm_compute; reflexivity.
(*
discriminate.
Qed.
*)
Abort.
|
