Added option of turning off model generation in SI. Can be very expensive sometimes.

3 files changed, 13 insertions, 15 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index a3bb44ba..2f02f0e5 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -560,6 +560,7 @@ namespace Microsoft.Boogie {
     public int ProcedureCopyBound = 0;

     public int StratifiedInlining = 0;

     public int StratifiedInliningOption = 0;

+    public bool StratifiedInliningWithoutModels = false; // disable model generation for SI

     public bool UseUnsatCoreForInlining = false;

     public int RecursionBound = 500;

     public string inferLeastForUnsat = null;

diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index 653b2c15..036b1f4a 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -43,12 +43,12 @@ namespace Microsoft.Boogie.SMTLib
 

     public bool ExpectingModel()

     {

-      return CommandLineOptions.Clo.PrintErrorModel >= 1 ||

-             CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||

-             CommandLineOptions.Clo.ModelViewFile != null ||

-             CommandLineOptions.Clo.ContractInfer ||

-             CommandLineOptions.Clo.LazyInlining > 0 ||

-             CommandLineOptions.Clo.StratifiedInlining > 0;

+        return CommandLineOptions.Clo.PrintErrorModel >= 1 ||

+               CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||

+               CommandLineOptions.Clo.ModelViewFile != null ||

+               CommandLineOptions.Clo.ContractInfer ||

+               CommandLineOptions.Clo.LazyInlining > 0 ||

+               (CommandLineOptions.Clo.StratifiedInlining > 0 && !CommandLineOptions.Clo.StratifiedInliningWithoutModels);

     }

 

     public void AddSolverArgument(string s)

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index df46ad50..e1c5ce13 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -3417,15 +3417,16 @@ namespace VC
             public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel)

             {

               //if (procBoundingMode) return; // shaz hack

+                Contract.Assert(CommandLineOptions.Clo.StratifiedInliningWithoutModels || errModel != null);

 

                 candidatesToExpand = new List<int>();

 

+                Model model = null;

+                if (errModel != null) model = errModel.ToModel();

+

                 //Contract.Requires(cce.NonNullElements(labels));

                 if (underapproximationMode)

                 {

-                    if (errModel == null)

-                        return;

-                    Model model = errModel.ToModel();

                     var cex = GenerateTraceMain(labels, model, mvInfo);

                     Debug.Assert(candidatesToExpand.Count == 0);

                     if (cex != null) {

@@ -3437,15 +3438,13 @@ namespace VC
                 }

                 

                 Contract.Assert(calls != null);

-                Contract.Assert(errModel != null);

 

-                GenerateTraceMain(labels, errModel.ToModel(), mvInfo);

+                GenerateTraceMain(labels, model, mvInfo);

             }

 

             // Construct the interprocedural trace

             private Counterexample GenerateTraceMain(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo)

             {

-                Contract.Requires(errModel != null);

                 Contract.Requires(cce.NonNullElements(labels));

                 if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null)

                 {

@@ -3484,7 +3483,6 @@ namespace VC
             private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo,

                                                  int candidateId, List<Tuple<int,int>> orderedStateIds, Implementation procImpl)

             {

-                Contract.Requires(errModel != null);

                 Contract.Requires(cce.NonNullElements(labels));

                 Contract.Requires(procImpl != null);

 

@@ -3535,7 +3533,6 @@ namespace VC
                                   Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples)

             {

                 Contract.Requires(cce.NonNullElements(labels));

-                Contract.Requires(errModel != null);

                 Contract.Requires(b != null);

                 Contract.Requires(traceNodes != null);

                 Contract.Requires(trace != null);

@@ -3579,7 +3576,7 @@ namespace VC
                           }

                         }

 

-                        if (calleeName.StartsWith(recordProcName))

+                        if (calleeName.StartsWith(recordProcName) && errModel != null)

                         {

                             var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];