From 31ec9bc299901a1a85abbd091c3293af00354030 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Thu, 31 Mar 2016 09:10:34 -0700
Subject: Fix issue 75. Adjust the fuel for existentials to use more fuel in an
 assume context and less in an assert.

---
 Test/dafny4/Bug75.dfy | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 Test/dafny4/Bug75.dfy

(limited to 'Test/dafny4/Bug75.dfy')

diff --git a/Test/dafny4/Bug75.dfy b/Test/dafny4/Bug75.dfy
new file mode 100644
index 00000000..37d35f77
--- /dev/null
+++ b/Test/dafny4/Bug75.dfy
@@ -0,0 +1,50 @@
+// RUN: %dafny /compile:0  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate R1(x:int, y:int) { x > 0 ==> R2(x - 1) }
+predicate R2(x:int) { exists y :: R1(x, y) }
+
+lemma L1(x:int)
+{
+    assume R2(x);
+    assert exists y :: R1(x, y); // FAILS
+}
+
+lemma L2(x:int)
+    requires R2(x); // Oddly, adding this requires fixes the problem
+{
+    assume R2(x);
+    assert exists y :: R1(x, y); // SUCCEEDS
+}
+
+// this predicate says that the first "n" elements of "s"
+
+// are in strictly increasing order
+
+predicate method Increasing(s: seq<int>, n: nat)
+  requires n <= |s|
+{
+  n < 2 ||
+  (s[n-2] < s[n-1] && Increasing(s, n-1))
+} 
+
+method Extend(s: seq<int>, n: nat) returns (n': nat)
+  requires n < |s|
+  requires forall i :: 0 <= i < n ==> Increasing(s, i)
+  ensures n <= n' <= |s|
+  ensures forall j :: 0 <= j < n' ==> Increasing(s, j)
+{
+  if 2 <= n && s[n-2] < s[n-1] {
+    n' := n + 1;
+  } else {
+    n' := n;
+  }
+}
+
+function pred(i:int):int { i - 1 }
+predicate f(a:int, s:int)            { (a <= 0 || (exists s0 :: f(pred(a), s0))) }
+
+lemma Fuel1(a:int, s:int)
+{
+    assert  f(a, s) <==> (a <= 0 || (exists s0 :: f(pred(a), s0))); // FAILS
+}
-- 
cgit v1.2.3