Add expected tests

Author: qinheping

tests/expected/quantifiers/assert_with_exists_fail.expected

@@ -0,0 +1,4 @@
+- Status: FAILURE\
+- Description: "assertion with exists"\
+
+VERIFICATION:- FAILED

tests/expected/quantifiers/assert_with_exists_fail.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+extern crate kani;
+use kani::kani_exists;
+
+#[kani::proof]
+fn exists_assert_harness() {
+    let j = kani::any();
+    kani::assume(j > 1);
+    kani::assert(kani::exists!(|i in (3,5)| i < j ), "assertion with exists");
+}

tests/expected/quantifiers/assert_with_exists_pass.expected

@@ -0,0 +1,4 @@
+- Status: SUCCESS\
+- Description: "assertion with exists"\
+     
+VERIFICATION:- SUCCESSFUL

tests/expected/quantifiers/assert_with_exists_pass.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+extern crate kani;
+use kani::kani_exists;
+
+#[kani::proof]
+fn exists_assert_harness() {
+    let j = kani::any();
+    kani::assume(j > 2);
+    kani::assert(kani::exists!(|i in (2,5)| i < j ), "assertion with exists");
+}

tests/expected/quantifiers/assert_with_forall_fail.expected

@@ -0,0 +1,5 @@
+- Status: FAILURE\
+- Description: "assertion with forall"\
+
+VERIFICATION:- FAILED
+

tests/expected/quantifiers/assert_with_forall_fail.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+extern crate kani;
+use kani::kani_forall;
+
+#[kani::proof]
+fn forall_assert_harness() {
+    let j = kani::any();
+    kani::assume(j > 3);
+    kani::assert(kani::forall!(|i in (2,5)| i < j ), "assertion with forall");
+}

tests/expected/quantifiers/assert_with_forall_pass.expected

@@ -0,0 +1,4 @@
+- Status: SUCCESS\
+- Description: "assertion with forall"\
+     
+VERIFICATION:- SUCCESSFUL

tests/expected/quantifiers/assert_with_forall_pass.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+extern crate kani;
+use kani::kani_forall;
+
+#[kani::proof]
+fn forall_assert_harness() {
+    let j = kani::any();
+    kani::assume(j > 5);
+    kani::assert(kani::forall!(|i in (2,5)| i < j ), "assertion with forall");
+}

tests/expected/quantifiers/assume_with_exists_fail.expected

@@ -0,0 +1,4 @@
+- Status: FAILURE\
+- Description: "assume with exists"\
+
+VERIFICATION:- FAILED

tests/expected/quantifiers/assume_with_exists_fail.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+extern crate kani;
+use kani::kani_exists;
+
+#[kani::proof]
+fn exists_assume_harness() {
+    let j = kani::any();
+    kani::assume(kani::exists!(|i in (2,4)| i == j));
+    kani::assert(j == 3, "assume with exists");
+}