Merge branch 'upstream' into dfsg_free

1 files changed, 34 insertions, 2 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 1f010757..19438924 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -85,6 +85,7 @@ namespace Microsoft.Boogie {
     public string RequestId;
     public abstract byte[] Checksum { get; }
     public byte[] SugaredCmdChecksum;
+    public bool IsAuxiliaryCexForDiagnosingTimeouts;
 
     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
 
@@ -313,7 +314,7 @@ namespace Microsoft.Boogie {
     public abstract int GetLocation();
   }
 
-  public class CounterexampleComparer : IComparer<Counterexample> {
+  public class CounterexampleComparer : IComparer<Counterexample>, IEqualityComparer<Counterexample> {
 
     private int Compare(List<Block> bs1, List<Block> bs2)
     {
@@ -375,6 +376,16 @@ namespace Microsoft.Boogie {
       }
       return -1;
     }
+
+    public bool Equals(Counterexample x, Counterexample y)
+    {
+      return Compare(x, y) == 0;
+    }
+
+    public int GetHashCode(Counterexample obj)
+    {
+      return 0;
+    }
   }
 
   public class AssertCounterexample : Counterexample {
@@ -1122,7 +1133,8 @@ namespace VC {
         }
         if (returnBlocks > 1) {
           string unifiedExitLabel = "GeneratedUnifiedExit";
-          Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(Token.NoToken));
+          Block unifiedExit;
+          unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken));         
           Contract.Assert(unifiedExit != null);
           foreach (Block b in impl.Blocks) {
             if (b.TransferCmd is ReturnCmd) {
@@ -1528,6 +1540,26 @@ namespace VC {
         PredicateCmd pc = (PredicateCmd)c.Clone();
         Contract.Assert(pc != null);
 
+        QKeyValue current = pc.Attributes;
+        while (current != null)
+        {
+          if (current.Key == "minimize" || current.Key == "maximize") {
+            Contract.Assume(current.Params.Count == 1);
+            var param = current.Params[0] as Expr;
+            Contract.Assume(param != null && (param.Type.IsInt || param.Type.IsReal || param.Type.IsBv));
+            current.ClearParams();
+            current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+          }
+          if (current.Key == "verified_under") {
+            Contract.Assume(current.Params.Count == 1);
+            var param = current.Params[0] as Expr;
+            Contract.Assume(param != null && param.Type.IsBool);
+            current.ClearParams();
+            current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+          }
+          current = current.Next;
+        }
+
         Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
         if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) {
           string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");