diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:03:09 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:03:09 -0400 |
commit | 618f037a466cd4392be6e1f4b20e248d58447456 (patch) | |
tree | 3c0b51de79e3537d3e94c8f1cca46f32d9a4b974 /Source/VCGeneration/Check.cs | |
parent | 636108e4c302a24ed658b5f09812010b30e36e95 (diff) | |
parent | 41082463d783d6f8d8a5aaf69bf459b57bca6000 (diff) |
Merge branch 'dfsg_free'
Diffstat (limited to 'Source/VCGeneration/Check.cs')
-rw-r--r-- | Source/VCGeneration/Check.cs | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 3c3b5cae..7bda0022 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -356,7 +356,7 @@ namespace Microsoft.Boogie { hasOutput = false; outputExn = null; this.handler = handler; - + thmProver.Reset(gen); SetTimeout(); proverStart = DateTime.UtcNow; @@ -386,6 +386,7 @@ namespace Microsoft.Boogie { // ----------------------------------------------------------------------------------------------- public abstract class ProverInterface { + public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) { Contract.Requires(prog != null); @@ -452,6 +453,10 @@ namespace Microsoft.Boogie { Undetermined, Bounded } + + public readonly ISet<VCExprVar> NamedAssumes = new HashSet<VCExprVar>(); + public ISet<string> UsedNamedAssumes { get; protected set; } + public class ErrorHandler { // Used in CheckOutcomeCore public virtual int StartingProcId() @@ -542,7 +547,7 @@ namespace Microsoft.Boogie { } // (assert vc) - public virtual void Assert(VCExpr vc, bool polarity) + public virtual void Assert(VCExpr vc, bool polarity, bool isSoft = false, int weight = 1) { throw new NotImplementedException(); } |