From e28c62b12194be07e3ecb3301e6b3e0336bcac2a Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Thu, 10 Mar 2011 01:20:05 +0000
Subject: Updated PrepareBoogieZip.bat to include BVD and smt2 Ignore
 duplicated else functions in models

---
 Binaries/PrepareBoogieZip.bat | 5 ++++-
 Source/VCGeneration/Check.cs  | 3 ++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/Binaries/PrepareBoogieZip.bat b/Binaries/PrepareBoogieZip.bat
index 38dff1d1..3c512aaa 100644
--- a/Binaries/PrepareBoogieZip.bat
+++ b/Binaries/PrepareBoogieZip.bat
@@ -11,22 +11,25 @@ for %%f in (
   AIFramework.dll             AIFramework.pdb
   Basetypes.dll               Basetypes.pdb
   Boogie.exe                  Boogie.pdb
+  BVD.exe                     BVD.pdb
   CodeContractsExtender.dll   CodeContractsExtender.pdb
   Core.dll                    Core.pdb
   Dafny.exe                   Dafny.pdb
   DafnyPipeline.dll           DafnyPipeline.pdb
   Graph.dll                   Graph.pdb
+  Model.dll                   Model.pdb
   ParserHelper.dll            ParserHelper.pdb
   Provers.Isabelle.dll        Provers.Isabelle.pdb
   Provers.Simplify.dll        Provers.Simplify.pdb
   Provers.SMTLib.dll          Provers.SMTLib.pdb
+  Provers.TPTP.dll            Provers.TPTP.pdb
   Provers.Z3.dll              Provers.Z3.pdb
   VCExpr.dll                  VCExpr.pdb
   VCGeneration.dll            VCGeneration.pdb
   DafnyPrelude.bpl
   DafnyRuntime.cs
   TypedUnivBackPred2.sx
-  UnivBackPred2.smt
+  UnivBackPred2.smt2
   UnivBackPred2.sx
 ) do (
   copy %%f %DEST_DIR%
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 67333752..5618fafa 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -507,7 +507,8 @@ namespace Microsoft.Boogie {
         var args = new Model.Element[arity];
         foreach (var l in tuples) {
           if (l.Count == 1) {
-            f.Else = elts[l[0]];
+            if (f.Else == null)
+              f.Else = elts[l[0]];
           } else {
             for (int i = 0; i < f.Arity; ++i)
               args[i] = elts[l[i]];
-- 
cgit v1.2.3