Integrated support for k-induction, implemented a while ago by Philipp Ruemmer but never previously committed.

1 files changed, 5 insertions, 0 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index da2c3a99..09549e55 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -417,6 +417,7 @@ namespace Microsoft.Boogie {
     public bool SoundnessSmokeTest = false;

     public string Z3ExecutablePath = null;

     public string CVC4ExecutablePath = null;

+    public int KInductionDepth = -1;

 

     public enum ProverWarnings {

       None,

@@ -1316,6 +1317,10 @@ namespace Microsoft.Boogie {
 			}

 			return true;

 

+        case "kInductionDepth":

+          ps.GetNumericArgument(ref KInductionDepth);

+          return true;

+

         default:

           bool optionValue = false;

           if (ps.CheckBooleanFlag("printUnstructured", ref optionValue)) {