Dafny: replaced the user-defined $ite function with Boogie's built-in if-then-else expression

1 files changed, 1 insertions, 8 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a28772ce..58f0e8eb 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3796,7 +3796,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr g = TrExpr(e.Test);

           Bpl.Expr thn = TrExpr(e.Thn);

           Bpl.Expr els = TrExpr(e.Els);

-          return translator.FunctionCall(expr.tok, BuiltinFunction.IfThenElse, translator.TrType(cce.NonNull(expr.Type)), g, thn, els);

+          return new NAryExpr(expr.tok, new IfThenElse(expr.tok), new ExprSeq(g, thn, els));

            

         } else if (expr is BoxingCastExpr) {

           BoxingCastExpr e = (BoxingCastExpr)expr;

@@ -4181,8 +4181,6 @@ namespace Microsoft.Dafny {
       IndexField,

       MultiIndexField,

       

-      IfThenElse,

-      

       Box,

       Unbox,

       

@@ -4299,11 +4297,6 @@ namespace Microsoft.Dafny {
           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "MultiIndexField", predef.FieldName(tok, predef.BoxType), args);

 

-        case BuiltinFunction.IfThenElse:

-          Contract.Assert(args.Length == 3);

-          Contract.Assert(typeInstantiation != null);

-          return FunctionCall(tok, "$ite", typeInstantiation, args);

-

         case BuiltinFunction.Box:

           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);