From b0c554caa4a5e885a214ceed13e2a86968846caa Mon Sep 17 00:00:00 2001
From: Jay Lorch <lorch@microsoft.com>
Date: Thu, 29 Jul 2021 11:27:49 -0700
Subject: [PATCH] Make compatible with Dafny 3.2.0

---
 ironfleet/README.md                                         | 6 +++---
 ironfleet/SConstruct                                        | 2 +-
 .../src/Dafny/Distributed/Common/Collections/Maps2.i.dfy    | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/ironfleet/README.md b/ironfleet/README.md
index 5280575d..b15ec643 100755
--- a/ironfleet/README.md
+++ b/ironfleet/README.md
@@ -37,7 +37,7 @@ IronFleet is licensed under the MIT license included in the [LICENSE](./LICENSE)
 
 To use Ironfleet, you'll need the following tools:
   * .NET 5.0 SDK (available at `https://dotnet.microsoft.com/download`)
-  * Dafny v3.1.0 (verifier, available at `https://github.com/dafny-lang/dafny`)
+  * Dafny v3.2.0 (verifier, available at `https://github.com/dafny-lang/dafny`)
   * python 2 or 3 (needed for running scons)
   * scons (installable by running `pip install scons`)
     
@@ -58,8 +58,8 @@ Expect this to take up to several hours, depending on your machine and how many
 cores you have available.  Also note that the prover's time limits are based on
 wall clock time, so if you run the verification on a slow machine, you may see a
 few timeouts not present in our build.  If that happens, try using a longer time
-limit for each verification; for example, using `--time-limit=60` makes the time
-limit 60 seconds instead of the default 30 seconds.
+limit for each verification; for example, using `--time-limit=120` makes the time
+limit 120 seconds instead of the default 60 seconds.
 
 Running scons will produce the following executables:
 ```
diff --git a/ironfleet/SConstruct b/ironfleet/SConstruct
index e788a315..0f127d47 100755
--- a/ironfleet/SConstruct
+++ b/ironfleet/SConstruct
@@ -29,7 +29,7 @@ AddOption('--no-verify',
 AddOption('--time-limit',
   dest='time_limit',
   type='int',
-  default=30,
+  default=60,
   action='store',
   help='Specify the time limit to use for each verification')
 
diff --git a/ironfleet/src/Dafny/Distributed/Common/Collections/Maps2.i.dfy b/ironfleet/src/Dafny/Distributed/Common/Collections/Maps2.i.dfy
index e6179561..56c87574 100755
--- a/ironfleet/src/Dafny/Distributed/Common/Collections/Maps2.i.dfy
+++ b/ironfleet/src/Dafny/Distributed/Common/Collections/Maps2.i.dfy
@@ -9,7 +9,7 @@ function maprange<KT,VT>(m:map<KT,VT>) : set<VT>
   set k | k in m :: m[k]
 }
 
-type imap2<!K1, K2, V> = imap<K1, imap<K2, V>>
+type imap2<!K1, !K2, V> = imap<K1, imap<K2, V>>
 
 predicate imap2total<K1(!new), K2(!new), V>(m:imap2<K1, K2, V>)
 {