diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-03-25 13:09:18 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-03-25 13:18:15 +0100 |
| commit | 3bdbbc287bc0138541db2bfabadd8196269c8f56 (patch) | |
| tree | ab8b2a1ced20c0ded71cdbfc7860a3ed0e373f93 /test-suite/failure | |
| parent | ebc509ed2d7a644aaf2a7d6d352d3f5bb80d25b0 (diff) | |
Test suite file for a bug in int31 arithmetic fixed a while ago.
Diffstat (limited to 'test-suite/failure')
| -rw-r--r-- | test-suite/failure/int31.v | 17 |
1 files changed, 17 insertions, 0 deletions
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. + |