Chalice: New regression test case.

2 files changed, 20 insertions, 0 deletions

diff --git a/Chalice/tests/regressions/internal-bug-1.chalice b/Chalice/tests/regressions/internal-bug-1.chalice
new file mode 100644
index 00000000..10caeebb
--- /dev/null
+++ b/Chalice/tests/regressions/internal-bug-1.chalice
@@ -0,0 +1,16 @@
+class Test {

+  var next: Test;

+  var elem: int;

+

+  predicate valid {

+    acc(elem) && acc(next) && 

+    (next != null ==> next.valid)

+  }

+  

+  function get(index:int):int

+    requires valid

+    // on 2012-02-21, a bug was reported that caused Chalice to crash with an

+    // InternalError for the following precondition.

+    requires unfolding valid in true

+  {0}

+}

diff --git a/Chalice/tests/regressions/internal-bug-1.output.txt b/Chalice/tests/regressions/internal-bug-1.output.txt
new file mode 100644
index 00000000..ea14d3e3
--- /dev/null
+++ b/Chalice/tests/regressions/internal-bug-1.output.txt
@@ -0,0 +1,4 @@
+Verification of internal-bug-1.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.