diff options
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/Simplify/Prover.cs | 8 | ||||
| -rw-r--r-- | Source/Provers/Simplify/ProverInterface.cs | 26 |
2 files changed, 17 insertions, 17 deletions
diff --git a/Source/Provers/Simplify/Prover.cs b/Source/Provers/Simplify/Prover.cs index b323b9b8..b789e588 100644 --- a/Source/Provers/Simplify/Prover.cs +++ b/Source/Provers/Simplify/Prover.cs @@ -480,7 +480,7 @@ namespace Microsoft.Boogie.Simplify { }
public override void AddAxioms(string s) {
- Contract.Requires(s != null);
+ //Contract.Requires(s != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
//ToWriteLine("(PROMPT_OFF)");
base.AddAxioms(s);
@@ -489,7 +489,7 @@ namespace Microsoft.Boogie.Simplify { }
public override void Feed(string s, int statementCount) {
- Contract.Requires(s != null);
+ //Contract.Requires(s != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
//ToWriteLine("(PROMPT_OFF)");
base.Feed(s, statementCount);
@@ -506,7 +506,7 @@ namespace Microsoft.Boogie.Simplify { }
protected override void DoBeginCheck(string descriptiveName, string formula) {
- Contract.Requires(descriptiveName != null);
+ //Contract.Requires(descriptiveName != null);
Contract.Requires(formula != null);
//simplify.Refresh();
//this.Comment("@@@@ Virtual Memory: " + simplify.PeakVirtualMemorySize64);
@@ -518,7 +518,7 @@ namespace Microsoft.Boogie.Simplify { }
public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler) {
- Contract.Requires(handler != null);
+ //Contract.Requires(handler != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
ProverOutcome outcome;
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs index ed2402b1..d300a685 100644 --- a/Source/Provers/Simplify/ProverInterface.cs +++ b/Source/Provers/Simplify/ProverInterface.cs @@ -108,7 +108,7 @@ namespace Microsoft.Boogie.Simplify { /// the comment (like, perhaps, a newline or "*/").
/// </summary>
public override void LogComment(string comment) {
- Contract.Requires(comment != null);
+ //Contract.Requires(comment != null);
LogComment(comment, false);
}
@@ -326,12 +326,12 @@ namespace Microsoft.Boogie.Simplify { /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
/// </summary>
public override void PushVCExpression(VCExpr vc) {
- Contract.Requires(vc != null);
+ //Contract.Requires(vc != null);
vcExprTranslator.AddAxiom(vcExprTranslator.translate(vc, 1));
}
public override string VCExpressionToString(VCExpr vc) {
- Contract.Requires(vc != null);
+ //Contract.Requires(vc != null);
Contract.Ensures(Contract.Result<string>() != null);
return vcExprTranslator.translate(vc, 1);
@@ -382,8 +382,8 @@ namespace Microsoft.Boogie.Simplify { private UnexpectedProverOutputException proverException;
public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {
- Contract.Requires(descriptiveName != null);
- Contract.Requires(vc != null);
+ //Contract.Requires(descriptiveName != null);
+ //Contract.Requires(vc != null);
Contract.Requires(handler != null);
this.NewProblem(descriptiveName);
this.proverException = null;
@@ -424,7 +424,7 @@ namespace Microsoft.Boogie.Simplify { }
public override Outcome CheckOutcome(ErrorHandler handler) {
- Contract.Requires(handler != null);
+ //Contract.Requires(handler != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
if (this.thmProver == null) {
@@ -613,14 +613,14 @@ namespace Microsoft.Boogie.Simplify { }
protected override ProverProcess CreateProverProcess(string proverPath) {
- Contract.Requires(proverPath != null);
+ //Contract.Requires(proverPath != null);
Contract.Ensures(Contract.Result<ProverProcess>() != null);
return new SimplifyProverProcess(proverPath);
}
protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {
- Contract.Requires(opts!=null);
+ //Contract.Requires(opts!=null);
Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
return new SimplifyVCExprTranslator(gen);
@@ -754,14 +754,14 @@ namespace Microsoft.Boogie.Simplify { public override string Lookup(VCExprVar var) {
- Contract.Requires(var != null);
+ //Contract.Requires(var != null);
Contract.Ensures(Contract.Result<string>() != null);
return Namer.Lookup(var);
}
public override string translate(VCExpr expr, int polarity) {
- Contract.Requires(expr != null);
+ //Contract.Requires(expr != null);
Contract.Ensures(Contract.Result<string>() != null);
Let2ImpliesMutator letImplier = new Let2ImpliesMutator(Gen);
@@ -813,8 +813,8 @@ namespace Microsoft.Boogie.Simplify { public class Factory : ProverFactory {
public override object SpawnProver(ProverOptions options, object ctxt) {
- Contract.Requires(options != null);
- Contract.Requires(ctxt != null);
+ //Contract.Requires(options != null);
+ //Contract.Requires(ctxt != null);
Contract.Ensures(Contract.Result<object>() != null);
return new SimplifyTheoremProver(options,
@@ -823,7 +823,7 @@ namespace Microsoft.Boogie.Simplify { }
public override object NewProverContext(ProverOptions options) {
- Contract.Requires(options != null);
+ //Contract.Requires(options != null);
Contract.Ensures(Contract.Result<object>() != null);
if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
|