diff options
author | 2016-02-12 16:47:51 -0800 | |
---|---|---|
committer | 2016-02-12 16:47:51 -0800 | |
commit | 7ce69481c0b6af79a6d6542989832cd90fc5690f (patch) | |
tree | a91488b8ad92bc69718f2d5fda1d44082a3959de /Source/VCGeneration/Check.cs | |
parent | abee810ceedbf551194788164fdf723edc511c0c (diff) | |
parent | 5fb565e439255ede7dc3653708af41678b6c1062 (diff) |
Merge branch 'master' of https://github.com/boogie-org/boogie
Diffstat (limited to 'Source/VCGeneration/Check.cs')
-rw-r--r-- | Source/VCGeneration/Check.cs | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 3c3b5cae..8c1ae407 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); @@ -356,10 +356,11 @@ namespace Microsoft.Boogie { hasOutput = false; outputExn = null; this.handler = handler; - + 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 +387,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); |