Implement if-then-else expression.

1 files changed, 34 insertions, 0 deletions

diff --git a/Test/test2/IfThenElse1.bpl b/Test/test2/IfThenElse1.bpl
new file mode 100644
index 00000000..8a867f50
--- /dev/null
+++ b/Test/test2/IfThenElse1.bpl
@@ -0,0 +1,34 @@
+type t1;
+
+procedure ok()
+{
+  var b:bool, x:int, y:int;
+
+  assert x == if b then x else x;
+  assert x == if true then x else y;
+}
+
+procedure ok2()
+{
+  var x:int, y:int;
+  var a:t1, b:t1, c:t1;
+
+  c := if x > y then a else b;
+  assert c == a || c == b;
+  assume x > y;
+  assert c == a;
+}
+
+procedure fail1()
+{
+  var b:bool, x:int, y:int;
+
+  assert x == if b then x else y;
+}
+
+procedure fail2()
+{
+  var b:bool, x:int, y:int;
+
+  assert x == if false then x else y;
+}