Boogie: Get rid of {:inline} attributes on axioms

1 files changed, 8 insertions, 27 deletions

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 4555f18c..4e9c5c10 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -1086,7 +1086,7 @@ namespace Microsoft.Boogie.VCExprAST {
         return null;

       }

 

-      Expansion exp = FindExpansion(app.Func);

+      var exp = app.Func.Body;

       if (exp == null)

         return null;

 

@@ -1099,11 +1099,12 @@ namespace Microsoft.Boogie.VCExprAST {
 

         // first bind the formals to VCExpr variables, which are later

         // substituted with the actual parameters

-        for (int i = 0; i < exp.formals.Length; ++i)

-          subst[BaseTranslator.BindVariable(cce.NonNull(exp.formals)[i])] = args[i];

+        var inParams = app.Func.InParams;

+        for (int i = 0; i < inParams.Length; ++i)

+          subst[BaseTranslator.BindVariable(inParams[i])] = args[i];

 

         // recursively translate the body of the expansion

-        translatedBody = BaseTranslator.Translate(exp.body);

+        translatedBody = BaseTranslator.Translate(exp);

       } finally {

         BaseTranslator.PopFormalsScope();

         BaseTranslator.PopBoundVariableScope();

@@ -1111,32 +1112,12 @@ namespace Microsoft.Boogie.VCExprAST {
       }

 

       // substitute the formals with the actual parameters in the body

-      Contract.Assert(typeArgs.Count == exp.TypeParameters.Length);

+      var tparms = app.Func.TypeParameters;

+      Contract.Assert(typeArgs.Count == tparms.Length);

       for (int i = 0; i < typeArgs.Count; ++i)

-        subst[exp.TypeParameters[i]] = typeArgs[i];

+        subst[tparms[i]] = typeArgs[i];

       SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);

       return substituter.Mutate(translatedBody, subst);

     }

-

-    private Expansion FindExpansion(Function func) {

-      Contract.Requires(func != null);

-      if (func.expansions == null)

-        return null;

-

-      Expansion exp = null;

-      foreach (Expansion e in func.expansions) {

-        Contract.Assert(e != null);

-        if (e.ignore == null || !GenerationOptions.IsAnyProverCommandSupported(e.ignore)) {

-          if (exp == null) {

-            exp = e;

-          } else {

-            System.Console.WriteLine("*** more than one possible expansion for {0}", func);

-            return null;

-          }

-        }

-      }

-

-      return exp;

-    }

   }

 }