summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/Check.cs
diff options
context:
space:
mode:
authorGravatar qunyanm <qunyanm@hotmail.com>2015-12-15 11:04:27 -0800
committerGravatar qunyanm <qunyanm@hotmail.com>2015-12-15 11:04:27 -0800
commiteb64daf4d3b3609bc47fa8f0f22069e7576c80c7 (patch)
tree668923025c0de2a99a4cb2b6ceb2133a014f1ed4 /Source/VCGeneration/Check.cs
parent277e5e7400330f4b26270fcaa4b0a70514b35104 (diff)
parent8938d00be93e780d54917c1448bc534702766fdf (diff)
Merge branch 'master' of https://github.com/boogie-org/boogie
Diffstat (limited to 'Source/VCGeneration/Check.cs')
-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;