From 152f26cf1bb467e6a9c9edb9cbf2871d7033a806 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 26 Oct 2015 13:08:30 +0100
Subject: [PATCH] test nested functions with nested if else
---
.../xlang/valid/NestedFunState7.scala | 27 +++++++++++++++++++
1 file changed, 27 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/valid/NestedFunState7.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunState7.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunState7.scala
new file mode 100644
index 000000000..ff2418a0c
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunState7.scala
@@ -0,0 +1,27 @@
+import leon.lang._
+
+object NestedFunState7 {
+
+ def test(x: BigInt): BigInt = {
+
+ var a = BigInt(0)
+
+ def defCase(): Unit = {
+ a = 100
+ }
+
+ if(x >= 0) {
+ a = 2*x
+ if(a < 100) {
+ a = 100 - a
+ } else {
+ defCase()
+ }
+ } else {
+ defCase()
+ }
+
+ a
+ } ensuring(res => res >= 0 && res <= 100)
+
+}
--
GitLab