From 1ed46d5269b5f9a0b3631b7cbb9c015e79ceeee1 Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Wed, 26 Jun 2024 12:17:00 -0500
Subject: [PATCH] Add a test on which SMT2 fail with quantifers in nested loop
 contracts

---
 .../quantifiers-loop-fail/main.c              | 27 +++++++++++++++++++
 .../quantifiers-loop-fail/test.desc           | 13 +++++++++
 2 files changed, 40 insertions(+)
 create mode 100644 regression/contracts-dfcc/quantifiers-loop-fail/main.c
 create mode 100644 regression/contracts-dfcc/quantifiers-loop-fail/test.desc

diff --git a/regression/contracts-dfcc/quantifiers-loop-fail/main.c b/regression/contracts-dfcc/quantifiers-loop-fail/main.c
new file mode 100644
index 00000000000..f44af096f58
--- /dev/null
+++ b/regression/contracts-dfcc/quantifiers-loop-fail/main.c
@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdbool.h>
+
+#define N 16
+
+void main()
+{
+  int a[N];
+  a[10] = 0;
+  bool flag = true;
+  for(int j = 0; j < N; ++j)
+    __CPROVER_loop_invariant(j <= N)
+    {
+      for(int i = 0; i < N; ++i)
+        // clang-format off
+        __CPROVER_assigns(i, __CPROVER_object_whole(a))
+        __CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall {
+          int k;
+          (0 <= k && k <= N) ==> (k<i ==> a[k] == 1)
+        })
+        // clang-format on
+        {
+          a[i] = 1;
+        }
+    }
+  assert(a[10] == 1);
+}
diff --git a/regression/contracts-dfcc/quantifiers-loop-fail/test.desc b/regression/contracts-dfcc/quantifiers-loop-fail/test.desc
new file mode 100644
index 00000000000..e54dd9ed35a
--- /dev/null
+++ b/regression/contracts-dfcc/quantifiers-loop-fail/test.desc
@@ -0,0 +1,13 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts _ --smt2
+^EXIT=6$
+^SIGNAL=0$
+^SMT2 solver returned error message:$
+^.*\"line \d+ column \d+: unknown constant .*$
+^VERIFICATION ERROR$
+--
+^warning: ignoring
+--
+This test case checks the handling of quantifiers in a nested loop's
+loop contracts.