1 files changed, 14 insertions, 2 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 3c3b5cae..da445a00 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -346,7 +346,7 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
+    public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, IList<VCExprVar> namedAssumeVars = null) {
       Contract.Requires(descriptiveName != null);
       Contract.Requires(vc != null);
       Contract.Requires(handler != null);
@@ -357,9 +357,18 @@ namespace Microsoft.Boogie {
       outputExn = null;
       this.handler = handler;
 
-      thmProver.Reset(gen);
+      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);
+      }
       SetTimeout();
       proverStart = DateTime.UtcNow;
+      thmProver.NamedAssumeVars = namedAssumeVars;
       thmProver.BeginCheck(descriptiveName, vc, handler);
       //  gen.ClearSharedFormulas();    PR: don't know yet what to do with this guy
 
@@ -386,6 +395,9 @@ namespace Microsoft.Boogie {
   // -----------------------------------------------------------------------------------------------
 
   public abstract class ProverInterface {
+
+    public IList<VCExprVar> NamedAssumeVars;
+
     public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
       Contract.Requires(prog != null);