From cc2267634bb0ebec11dcf240a3099ee3a1adb006 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 26 Mar 2021 13:26:49 -0400
Subject: Add non-performance-based test

---
 test-suite/bugs/closed/bug_14011.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/test-suite/bugs/closed/bug_14011.v b/test-suite/bugs/closed/bug_14011.v
index c1d3ce7a89..ccbeca792d 100644
--- a/test-suite/bugs/closed/bug_14011.v
+++ b/test-suite/bugs/closed/bug_14011.v
@@ -1,5 +1,14 @@
 (** Test that Ltac2 Array.init doesn't compute the first argument twice, and has the correct asymptotics when nested *)
 Require Import Ltac2.Ltac2.
+
+(** Non-performance-based test *)
+Ltac2 foo () :=
+  let x := { contents := 0 } in
+  let _ := Array.init 1 (fun _ => x.(contents) := Int.add 1 (x.(contents))) in
+  Control.assert_true (Int.equal 1 (x.(contents))).
+
+Ltac2 Eval foo ().
+
 Ltac2 Type rec singleton := [ Single (int) | Arr (singleton array) ].
 Ltac2 rec init_rec (n : int) :=
   match Int.equal n 0 with
-- 
cgit v1.2.3