Factored out the closure for codeexpr conversion so that it can be reused.

Enabled it in stratified inlining.

1 files changed, 3 insertions, 0 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index ceea2477..aeeb0507 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -266,6 +266,9 @@ 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));