new option to disable checking for loop maintained invariants - this leads to an underapproximation that helps to speedup houdini refutation of candidates

1 files changed, 4 insertions, 2 deletions

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;