Add another test

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
+}

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);
+}