refactored StratifiedInline.GenerateVC to use GenerateVCAux instead of GenerateVC

1 files changed, 7 insertions, 4 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index aeeb0507..bf3f267f 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -266,16 +266,19 @@ namespace VC {
       VCExpressionGenerator gen = proverInterface.VCExprGen;

       var exprGen = proverInterface.Context.ExprGen;

       var translator = proverInterface.Context.BoogieExprTranslator;

-      VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, proverInterface.Context);

-      translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition);

-

+      

       VCExpr controlFlowVariableExpr = null;

       if (!CommandLineOptions.Clo.UseLabels) {

         controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));

         controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable);

         vcgen.InstrumentCallSites(impl);

       }

-      vcexpr = gen.Not(vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context));

+      

+      label2absy = new Dictionary<int, Absy>();

+      VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, proverInterface.Context);

+      translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition); 

+      vcexpr = gen.Not(vcgen.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverInterface.Context));

+      

       if (controlFlowVariableExpr != null) {

         VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));

         VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));