From 6dfa82655aa7cb35bae6904e05887cdf960c6319 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Mon, 13 Jul 2015 11:55:06 -0700
Subject: Fix multiple tests that relied on z3 triggering on $Box

Found by enabling auto-generated triggers and looking for failing tests
---
 Test/dafny1/BDD.dfy | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Test/dafny1/BDD.dfy')

diff --git a/Test/dafny1/BDD.dfy b/Test/dafny1/BDD.dfy
index 252164db..59dc3092 100644
--- a/Test/dafny1/BDD.dfy
+++ b/Test/dafny1/BDD.dfy
@@ -55,6 +55,7 @@ module SimpleBDD
 		 node := if s[n-i] then node.t else node.f;
 		 i := i - 1;
 	   }
+           assert s[n-i..] == [];
 	   b := node.b;
 	 }
    }
-- 
cgit v1.2.3