diff options
author | Valentin Wüstholz <wuestholz@gmail.com> | 2016-03-03 17:32:31 -0600 |
---|---|---|
committer | Valentin Wüstholz <wuestholz@gmail.com> | 2016-03-03 17:32:31 -0600 |
commit | 502942a53a6db2b3a900d7570807216372d49ad0 (patch) | |
tree | 494530d18be4957b05379f3bc4b12d1f83e22e9e /Source/VCGeneration/Check.cs | |
parent | 8e5a0356cc3122e780fe28300dbad5ade2c13197 (diff) |
Improve support for optimization and identifying unnecessary assumes.
Diffstat (limited to 'Source/VCGeneration/Check.cs')
-rw-r--r-- | Source/VCGeneration/Check.cs | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 8c1ae407..ae4d158a 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, IList<VCExprVar> namedAssumeVars = null) { + public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); Contract.Requires(handler != null); @@ -360,7 +360,6 @@ namespace Microsoft.Boogie { 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 @@ -388,8 +387,6 @@ 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); @@ -546,7 +543,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(); } |