summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/VCGeneration/Check.cs12
1 files 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;