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(-)

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