From 08134b2a95acb34813333a3cc980f4f35d811885 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Thu, 19 Sep 2024 11:22:03 -0700
Subject: [PATCH] Add another test

---
 tests/expected/llbc/basic1/expected | 15 +++++++++++++++
 tests/expected/llbc/basic1/test.rs  | 20 ++++++++++++++++++++
 2 files changed, 35 insertions(+)
 create mode 100644 tests/expected/llbc/basic1/expected
 create mode 100644 tests/expected/llbc/basic1/test.rs

diff --git a/tests/expected/llbc/basic1/expected b/tests/expected/llbc/basic1/expected
new file mode 100644
index 000000000000..9cb0bef6f7c6
--- /dev/null
+++ b/tests/expected/llbc/basic1/expected
@@ -0,0 +1,15 @@
+fn test::select(@1: bool, @2: i32, @3: i32) -> i32
+{
+    let @0: i32; // return
+    let @1: bool; // arg #1
+    let @2: i32; // arg #2
+    let @3: i32; // arg #3
+
+    if copy (@1) {
+        @0 := copy (@2)
+    }
+    else {
+        @0 := copy (@3)
+    }
+    return
+}
diff --git a/tests/expected/llbc/basic1/test.rs b/tests/expected/llbc/basic1/test.rs
new file mode 100644
index 000000000000..1d0147964a60
--- /dev/null
+++ b/tests/expected/llbc/basic1/test.rs
@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zaeneas
+
+//! This test checks that Kani's LLBC backend handles basic expressions, in this
+//! case an if condition
+
+fn select(s: bool, x: i32, y: i32) -> i32 {
+    if s {
+        x
+    } else {
+        y
+    }
+}
+
+
+#[kani::proof]
+fn main() {
+    let _ = select(true, 3, 7);
+}