diff options
author | Valentin Wüstholz <wuestholz@gmail.com> | 2015-12-02 12:02:43 -0600 |
---|---|---|
committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-12-02 12:03:46 -0600 |
commit | 9b355c4e494bc6427e3d165288c09e113a86000a (patch) | |
tree | 167d3be9c59fd32595ed0a5ad60d01c43b25e750 /Source/VCGeneration | |
parent | 3e4a58021e7f9b2bd31dd195f9a7b2f02d5b4c02 (diff) |
Remove workaround for older versions of Z3.
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r-- | Source/VCGeneration/Check.cs | 12 |
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; |