From 679af7cd0963341cbb057cf9049c81b515a8fa26 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 17 Dec 2013 13:56:41 -0800
Subject: Don't inline opaque functions. Added a verifying example with opaque
 functions and explicit proofs.

---
 Test/dafny3/Answer      | 4 ++++
 Test/dafny3/runtest.bat | 1 +
 2 files changed, 5 insertions(+)

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index f326d2f9..5b7357e6 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -54,3 +54,7 @@ Dafny program verifier finished with 10 verified, 0 errors
 -------------------- InfiniteTrees.dfy --------------------
 
 Dafny program verifier finished with 88 verified, 0 errors
+
+-------------------- OpaqueTrees.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
index 7a3d3a20..9bce80c5 100644
--- a/Test/dafny3/runtest.bat
+++ b/Test/dafny3/runtest.bat
@@ -9,6 +9,7 @@ for %%f in (
   SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy
   InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy
   Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy
+  OpaqueTrees.dfy
 ) do (
   echo.
   echo -------------------- %%f --------------------
-- 
cgit v1.2.3