diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 7 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 2 |
2 files changed, 8 insertions, 1 deletions
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index d60e7323..6808be61 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -228,6 +228,7 @@ namespace Microsoft.Boogie public int LazyInlining = 0;
public int StratifiedInlining = 0;
public int StratifiedInliningOption = 0;
+ public int RecursionBound = 500;
public string CoverageReporterPath = null;
public enum TypeEncoding { None, Predicates, Arguments, Monomorphic };
@@ -993,6 +994,12 @@ namespace Microsoft.Boogie }
}
break; + case "-recursionBound":
+ case "/recursionBound":
+ if (ps.ConfirmArgumentCount(1)) {
+ RecursionBound = Int32.Parse((!)args[ps.i]);
+ }
+ break; case "-coverageReporter":
case "/coverageReporter":
if (ps.ConfirmArgumentCount(1)) {
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index b77117ff..42626ed7 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2010,7 +2010,7 @@ namespace VC { int bound = 1;
bool done = false;
- while (bound < 500 && !done)
+ while (bound < CommandLineOptions.Clo.RecursionBound && !done)
{
while (true)
{
|