stratified inlining: added option of turning off CheckAssumptions

1 files changed, 7 insertions, 0 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 303a78ce..ef12ec01 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -672,6 +672,8 @@ namespace VC
             private List<int> numAxiomsPushed;

             // Api-based theorem prover

             private ApiProverInterface TheoremProver;

+            // Use checkAssumptions?

+            public static bool UseCheckAssumptions = true;

 

             public ApiChecker(VCExpr vcMain, StratifiedInliningErrorReporter reporter, Checker checker)

             {

@@ -739,6 +741,11 @@ namespace VC
             

             public override Outcome CheckAssumptions(List<VCExpr> assumptions)

             {

+                if (!UseCheckAssumptions)

+                {

+                    return base.CheckAssumptions(assumptions);

+                }

+

                 if (assumptions.Count == 0)

                 {

                     return CheckVC();