From f97656456a74564cdf96633c3f46223d39e2c6f2 Mon Sep 17 00:00:00 2001
From: qunyanm <qunyanm@hotmail.com>
Date: Mon, 16 Nov 2015 11:03:28 -0800
Subject: Use the EndCurly token when creating the ReturnCmd for unifiedExit

When there are more than one exit blocks, an unified exit block is
created which includes a ReturnCmd. However, the ReturnCmd is created
with NoToken. This causes the line/column number reported for a failed
postcondition to be (0,0). The right token should be the EndCurly since
the ReturnCmd is in the exit block.
---
 Source/VCGeneration/ConditionGeneration.cs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Source')

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 6a2eec29..19438924 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1133,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) {
-- 
cgit v1.2.3


From 9b355c4e494bc6427e3d165288c09e113a86000a Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Wed, 2 Dec 2015 12:02:43 -0600
Subject: Remove workaround for older versions of Z3.

---
 Source/VCGeneration/Check.cs | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

(limited to 'Source')

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index da445a00..8c1ae407 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -356,16 +356,8 @@ namespace Microsoft.Boogie {
       hasOutput = false;
       outputExn = null;
       this.handler = handler;
-
-      if (namedAssumeVars != null && namedAssumeVars.Any())
-      {
-        // TODO(wuestholz): Avoid doing a full reset. This is currently necessary for old versions of Z3 due to a bug.
-        thmProver.FullReset(gen);
-      }
-      else
-      {
-        thmProver.Reset(gen);
-      }
+      
+      thmProver.Reset(gen);
       SetTimeout();
       proverStart = DateTime.UtcNow;
       thmProver.NamedAssumeVars = namedAssumeVars;
-- 
cgit v1.2.3


From 8938d00be93e780d54917c1448bc534702766fdf Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Thu, 3 Dec 2015 09:39:44 -0600
Subject: Remove unused file.

---
 Source/version.ssc | 12 ------------
 1 file changed, 12 deletions(-)
 delete mode 100644 Source/version.ssc

(limited to 'Source')

diff --git a/Source/version.ssc b/Source/version.ssc
deleted file mode 100644
index 5bdcf170..00000000
--- a/Source/version.ssc
+++ /dev/null
@@ -1,12 +0,0 @@
-// ==++==
-// 
-//   
-// 
-// ==--==
-// Warning: Automatically generated file. DO NOT EDIT
-// Generated at Dienstag, 5. Juli 2011 11:26:45
-
-using System.Reflection;
-[assembly: AssemblyVersion("2.2.30705.1126")]
-[assembly: AssemblyFileVersion("2.2.30705.1126")]
-
-- 
cgit v1.2.3