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/dafny4/CoqArt-InsertionSort.dfy | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Test/dafny4/CoqArt-InsertionSort.dfy')

diff --git a/Test/dafny4/CoqArt-InsertionSort.dfy b/Test/dafny4/CoqArt-InsertionSort.dfy
index efd01537..99e0f0b1 100644
--- a/Test/dafny4/CoqArt-InsertionSort.dfy
+++ b/Test/dafny4/CoqArt-InsertionSort.dfy
@@ -151,6 +151,7 @@ lemma existence_proof(l: List<int>)
 {
   match l {
     case Nil =>
+      assert sorted(Nil);
     case Cons(x, m) =>
       existence_proof(m);
       var m' :| equiv(m, m') && sorted(m');
-- 
cgit v1.2.3