Update tests

Author: tautschnig

tests/kani/Quantifiers/array_fixme.rs tests/kani/Quantifiers/array.rstests/kani/Quantifiers/array_fixme.rs renamed to tests/kani/Quantifiers/array.rs

@@ -1,8 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! FIXME: <https://github.com/model-checking/kani/issues/4019>
-
 extern crate kani;
 use kani::kani_forall;
 

tests/kani/Quantifiers/contracts_fixme.rs tests/kani/Quantifiers/contracts.rstests/kani/Quantifiers/contracts_fixme.rs renamed to tests/kani/Quantifiers/contracts.rs

@@ -2,8 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
 
-//! FIXME: <https://github.com/model-checking/kani/issues/4019>
-
 #![feature(proc_macro_hygiene)]
 #![feature(stmt_expr_attributes)]
 extern crate kani;

tests/kani/Quantifiers/no_array.rs

@@ -18,9 +18,34 @@ fn forall_assume_harness() {
     kani::assert(j > 4, "");
 }
 
+fn comp(x: usize, y: usize) -> bool {
+    x > y
+}
+
+#[kani::proof]
+fn forall_function_harness() {
+    let j = kani::any();
+    kani::assume(j > 5);
+    kani::assert(kani::forall!(|i in (2,5)| comp(j, i) ), "");
+}
+
 #[kani::proof]
 fn exists_assert_harness() {
     let j = kani::any();
     kani::assume(j > 2);
     kani::assert(kani::exists!(|i in (2,5)| i < j ), "");
 }
+
+#[kani::proof]
+fn exists_assume_harness() {
+    let j = kani::any();
+    kani::assume(kani::exists!(|i in (2,4)| i == j));
+    kani::assert(j == 3 || j == 2, "");
+}
+
+#[kani::proof]
+fn exists_function_harness() {
+    let j = kani::any();
+    kani::assume(j > 2);
+    kani::assert(kani::exists!(|i in (2,5)| comp(j, i) ), "");
+}