diff options
| author |  qunyanm <qunyanm@hotmail.com> | 2015-12-15 11:04:27 -0800 |
|---|---|---|
| committer | qunyanm <qunyanm@hotmail.com> | 2015-12-15 11:04:27 -0800 |
| commit | eb64daf4d3b3609bc47fa8f0f22069e7576c80c7 (patch) | |
| tree | 668923025c0de2a99a4cb2b6ceb2133a014f1ed4 /Source | |
| parent | 277e5e7400330f4b26270fcaa4b0a70514b35104 (diff) | |
| parent | 8938d00be93e780d54917c1448bc534702766fdf (diff) | |
Merge branch 'master' of https://github.com/boogie-org/boogie
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 12 | ||||
| -rw-r--r-- | Source/version.ssc | 12 |
2 files changed, 2 insertions, 22 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; 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")] - |