Simple VC generation for SI

1 files changed, 2 insertions, 0 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 98bb95d2..e9e6b60e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -480,6 +480,7 @@ namespace Microsoft.Boogie {
     public bool UseSmtOutputFormat = false;

     public bool WeakArrayTheory = false;

     public bool UseLabels = true;

+    public bool SIBoolControlVC = false;

     public bool MonomorphicArrays {

       get {

         return UseArrayTheory || TypeEncodingMethod == TypeEncoding.Monomorphic;

@@ -1417,6 +1418,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) || 

               ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||

               ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||

+              ps.CheckBooleanFlag("boolControlVC", ref SIBoolControlVC, true) ||

               ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||

               ps.CheckBooleanFlag("explainHoudini", ref ExplainHoudini) ||

               ps.CheckBooleanFlag("reverseHoudiniWorklist", ref ReverseHoudiniWorklist) ||