From 3bdbbc287bc0138541db2bfabadd8196269c8f56 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 25 Mar 2016 13:09:18 +0100 Subject: Test suite file for a bug in int31 arithmetic fixed a while ago. --- test-suite/failure/int31.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 test-suite/failure/int31.v (limited to 'test-suite/failure') diff --git a/test-suite/failure/int31.v b/test-suite/failure/int31.v new file mode 100644 index 000000000..b1d112247 --- /dev/null +++ b/test-suite/failure/int31.v @@ -0,0 +1,17 @@ +Require Import Int31 BigN. + +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. + -- cgit v1.2.3