aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/int31.v
blob: ed4c9f9c78213def384276afc6422f9d918fb486 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Require Import Int31 Cyclic31.

Open Scope int31_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 (add31 (addmuldiv31 65 (add31 1 1) 2) 1).
Fail vm_compute; reflexivity.
(*
discriminate.
Qed.
*)
Abort.