From 0515894d328e74bbee85d53cae539c98edf7ba23 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Sun, 6 May 2012 19:25:57 +0000
Subject: [PATCH] example that illustrates bug with if condition, now fixed
---
testcases/regression/valid/Nested8.scala | 43 ++++++++++++++++++++++++
1 file changed, 43 insertions(+)
create mode 100644 testcases/regression/valid/Nested8.scala
diff --git a/testcases/regression/valid/Nested8.scala b/testcases/regression/valid/Nested8.scala
new file mode 100644
index 000000000..e8a05e40e
--- /dev/null
+++ b/testcases/regression/valid/Nested8.scala
@@ -0,0 +1,43 @@
+import leon.Utils._
+
+object Nested8 {
+
+ def foo(a: Int): Int = {
+ require(a > 0)
+
+ def bar(b: Int): Int = {
+ if(a < b) {
+ def rec(c: Int): Int = {
+ require(c > 0)
+ c + b
+ } ensuring(_ > 0)
+ rec(2)
+ } else 3
+ }
+ bar(1)
+ } ensuring(_ > 0)
+
+ /*
+ def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+ */
+
+}
--
GitLab