From 3dd957cf440edf04504f6b0ca8b57fac64e813a7 Mon Sep 17 00:00:00 2001
From: Federico Poli <fpoli@users.noreply.github.com>
Date: Thu, 2 Feb 2023 13:57:16 +0100
Subject: [PATCH] Add test from issue #1286

---
 .../pass/generic/increasing.rs                | 22 +++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 prusti-tests/tests/verify_overflow/pass/generic/increasing.rs

diff --git a/prusti-tests/tests/verify_overflow/pass/generic/increasing.rs b/prusti-tests/tests/verify_overflow/pass/generic/increasing.rs
new file mode 100644
index 00000000000..3de35f6c404
--- /dev/null
+++ b/prusti-tests/tests/verify_overflow/pass/generic/increasing.rs
@@ -0,0 +1,22 @@
+use prusti_contracts::*;
+
+#[extern_spec]
+impl PartialOrd<i32> for i32{
+    #[pure]
+    #[ensures(result == (*self < *other))]
+    fn lt(&self, other: &i32) -> bool;
+}
+
+predicate! {
+    fn increasing<T: PartialOrd>(s: &[T]) -> bool {
+        forall(|i: usize, j: usize|
+            (i < j && j < s.len() ==> s[i] < s[j]))
+    }
+}
+
+fn test() {
+    let x = [1, 2, 3];
+    prusti_assert!(increasing(&x));
+}
+
+fn main() {}