diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 10 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 1 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 6 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 7 |
4 files changed, 20 insertions, 4 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 46f74004..22d48af0 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -398,6 +398,7 @@ namespace Microsoft.Boogie { public bool ContractInfer = false;
public bool ExplainHoudini = false;
public bool HoudiniOutputRefutedCandidates = false;
+ public bool DisableLoopInvMaintainedAssert = false;
public bool DebugParallelHoudini = false;
public bool HoudiniUseCrossDependencies = false;
public string StagedHoudini = null;
@@ -1173,6 +1174,12 @@ namespace Microsoft.Boogie { }
return true;
+ case "disableLoopInvMaintainedAssert":
+ if (ps.ConfirmArgumentCount(0)) {
+ DisableLoopInvMaintainedAssert = true;
+ }
+ return true;
+
case "debugParallelHoudini":
if (ps.ConfirmArgumentCount(0)) {
DebugParallelHoudini = true;
@@ -1668,6 +1675,9 @@ namespace Microsoft.Boogie { invariants
/outputRefuted
Outputs the refuted candidates
+ /disableLoopInvMaintainedAssert
+ Disables the loop invariant check to maintain the invariant after iteration.
+ This is an under-approximation feature.
---- Debugging and general tracing options ---------------------------------
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index f81150b1..34a32dfd 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -686,7 +686,6 @@ namespace Microsoft.Boogie }
}
-
/// <summary>
/// Given a resolved and type checked Boogie program, infers invariants for the program
/// and then attempts to verify it. Returns:
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index 3f4ef5ac..0cfa65d8 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -87,15 +87,17 @@ namespace Microsoft.Boogie.SMTLib string SolverStr = null;
if (ParseString(opt, "SOLVER", ref SolverStr)) {
switch (SolverStr) {
+ case "Z3":
case "z3":
Solver = SolverKind.Z3;
break;
+ case "CVC4":
case "cvc4":
Solver = SolverKind.CVC4;
- if (Logic.Equals("")) Logic = "ALL_SUPPORTED";
+ if (Logic.Equals("")) Logic = "ALL_SUPPORTED";
break;
default:
- ReportError("Invalid SOLVER value; must be 'z3' or 'cvc4'");
+ ReportError("Invalid SOLVER value; must be 'Z3' or 'CVC4'");
return false;
}
return true;
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index fd7a4f72..1aed2cba 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1944,7 +1944,12 @@ namespace VC { b.Attributes = c.Attributes;
b.ErrorData = c.ErrorData;
prefixOfPredicateCmdsInit.Add(b);
- b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);
+
+ if (CommandLineOptions.Clo.DisableLoopInvMaintainedAssert)
+ b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);
+ else
+ b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);
+
b.Attributes = c.Attributes;
b.ErrorData = c.ErrorData;
prefixOfPredicateCmdsMaintained.Add(b);
|