Implement if-then-else expression.

18 files changed, 372 insertions, 123 deletions

diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc
index c07db23b..ebc594f3 100644
--- a/Source/Core/AbsyExpr.ssc
+++ b/Source/Core/AbsyExpr.ssc
@@ -843,6 +843,8 @@ namespace Microsoft.Boogie
     T Visit(MapStore! mapStore);

     

     T Visit(TypeCoercion! typeCoercion);

+

+    T Visit(IfThenElse! ifThenElse);

   }

 

   public interface IAppliable

@@ -2895,6 +2897,97 @@ namespace Microsoft.Boogie
     }

   }

 

+

+

+  public class IfThenElse : IAppliable, AI.IFunctionSymbol {

+

+    public IToken! tok;

+

+    public IfThenElse(IToken! tok) {

+      this.tok = tok;

+    }

+

+    public string! FunctionName { get {

+      return "if-then-else";

+    } }

+

+    [Pure][Reads(ReadsAttribute.Reads.Nothing)]

+    public override bool Equals(object obj)

+    {

+      if (!(obj is IfThenElse)) return false;

+      return true;

+    }

+

+    [Pure] 

+    public override int GetHashCode()

+    {

+      return 1;

+    }

+

+    public void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext) 

+    {

+      stream.SetToken(ref this.tok);

+      assert args.Length == 3;

+      stream.Write("(if ");

+      ((!)args[0]).Emit(stream, 0x00, false);

+      stream.Write(" then ");

+      ((!)args[1]).Emit(stream, 0x00, false);

+      stream.Write(" else ");

+      ((!)args[2]).Emit(stream, 0x00, false);

+      stream.Write(")");

+    }

+

+    public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting) {

+      // PR: nothing?

+    }

+

+    public int ArgumentCount { get {

+      return 3;

+    } }

+

+    public Type Typecheck(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc) 

+    {

+      assert args.Length == 3;

+      // the default; the only binary operator with a type parameter is equality, but right

+      // we don't store this parameter because it does not appear necessary

+      tpInstantiation = SimpleTypeParamInstantiation.EMPTY;

+      Expr arg0 = (!)args[0];

+      Expr arg1 = (!)args[1];

+      Expr arg2 = (!)args[2];

+

+      if (!((!)arg0.Type).Unify(Type.Bool)) {

+        tc.Error(this.tok, "the first argument to if-then-else should be bool, not {0}", arg0.Type);

+      } else if (!((!)arg1.Type).Unify((!)arg2.Type)) {

+        tc.Error(this.tok, "branches of if-then-else have incompatible types {0} and {1}", arg1.Type, arg2.Type);

+      } else {

+        return arg1.Type;

+      }

+

+      return null;

+    }

+

+    /// <summary>

+    /// Returns the result type of the IAppliable, supposing the argument are of the correct types.

+    /// </summary>

+    public Type! ShallowType(ExprSeq! args) {

+      return ((!)args[1]).ShallowType;

+    }

+

+    public AI.IFunctionSymbol! AIFunctionSymbol { get { return this; } }

+    

+    public AI.AIType! AIType {

+      [Rep][ResultNotNewlyAllocated]

+      get {

+        return AI.Value.FunctionType(3);

+    } }

+    

+    public T Dispatch<T>(IAppliableVisitor<T>! visitor) {

+      return visitor.Visit(this);

+    }

+  }

+  

+

+

   public class BlockExpr : Expr

   {

     public VariableSeq! LocVars;

@@ -3254,3 +3347,4 @@ namespace Microsoft.Boogie
     }

   }

 }

+

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index eab10ff9..ab7e6c81 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -1291,6 +1291,7 @@ AtomExpression<out Expr! e>
                                                  e = new ExistsExpr(x, typeParams, ds, kv, trig, e); .)

         )

     ")"

+  | IfThenElseExpression<out e>

   )

   .

 

@@ -1352,6 +1353,15 @@ AttributeParameter<out object! o>
   )

   .

 

+IfThenElseExpression<out Expr! e>

+= (. IToken! tok;

+     Expr! e0, e1, e2; 

+     e = dummyExpr; .)

+  "if" (. tok = token; .) Expression<out e0> "then" Expression<out e1> "else" Expression<out e2>

+  (. e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); .)

+  .

+

+

 QuantifierBody<IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,

                out QKeyValue kv, out Trigger trig, out Expr! body>

 = (. trig = null; typeParams = new TypeVariableSeq ();

diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc
index a7453d09..95eb1a76 100644
--- a/Source/Core/Parser.ssc
+++ b/Source/Core/Parser.ssc
@@ -1,8 +1,3 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

 using PureCollections;

 using System.Collections;

 using System.Collections.Generic;

@@ -16,7 +11,7 @@ using Microsoft.Contracts;
 namespace BoogiePL {

 

 public class Parser {

-	const int maxT = 85;

+	const int maxT = 86;

 

 	const bool T = true;

 	const bool x = false;

@@ -299,7 +294,7 @@ private class BvBounds : Expr {
 			Get();

 			Type(out retTy);

 			retTyd = new TypedIdent(retTy.tok, "", retTy); 

-		} else Error(86);

+		} else Error(87);

 		if (t.kind == 25) {

 			Get();

 			Expression(out tmp);

@@ -307,7 +302,7 @@ private class BvBounds : Expr {
 			Expect(26);

 		} else if (t.kind == 7) {

 			Get();

-		} else Error(87);

+		} else Error(88);

 		if (retTyd == null) {

 		 // construct a dummy type for the case of syntax error

 		 tyd = new TypedIdent(token, "", new BasicType(token, SimpleType.Int));

@@ -451,7 +446,7 @@ private class BvBounds : Expr {
 			impl = new Implementation(x, x.val, typeParams,

 			                          Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null); 

 			

-		} else Error(88);

+		} else Error(89);

 		proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); 

 	}

 

@@ -555,7 +550,7 @@ private class BvBounds : Expr {
 			ty = new UnresolvedTypeIdentifier (tok, tok.val, args); 

 		} else if (t.kind == 15 || t.kind == 17) {

 			MapType(out ty);

-		} else Error(89);

+		} else Error(90);

 	}

 

 	static void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {

@@ -602,7 +597,7 @@ private class BvBounds : Expr {
 			Get();

 			Type(out ty);

 			Expect(9);

-		} else Error(90);

+		} else Error(91);

 	}

 

 	static void Ident(out IToken! x) {

@@ -631,7 +626,7 @@ private class BvBounds : Expr {
 		} else if (t.kind == 15 || t.kind == 17) {

 			MapType(out ty);

 			ts.Add(ty); 

-		} else Error(91);

+		} else Error(92);

 	}

 

 	static void MapType(out Bpl.Type! ty) {

@@ -803,7 +798,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			SpecPrePost(true, pre, post);

 		} else if (t.kind == 34 || t.kind == 35) {

 			SpecPrePost(false, pre, post);

-		} else Error(92);

+		} else Error(93);

 	}

 

 	static void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {

@@ -831,7 +826,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				SpecBody(out locals, out blocks);

 				Expect(7);

 				pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv)); 

-			} else Error(93);

+			} else Error(94);

 		} else if (t.kind == 35) {

 			Get();

 			tok = token; 

@@ -846,8 +841,8 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				SpecBody(out locals, out blocks);

 				Expect(7);

 				post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv)); 

-			} else Error(94);

-		} else Error(95);

+			} else Error(95);

+		} else Error(96);

 	}

 

 	static void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {

@@ -898,7 +893,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 			Expression(out e);

 			b = new Block(x,x.val,cs,new ReturnExprCmd(token,e)); 

-		} else Error(96);

+		} else Error(97);

 		Expect(7);

 	}

 

@@ -942,7 +937,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			CallCmd(out cn);

 			Expect(7);

 			c = cn; 

-		} else Error(97);

+		} else Error(98);

 	}

 

 	static void StmtList(out StmtList! stmtList) {

@@ -1026,7 +1021,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 45) {

 			BreakCmd(out bcmd);

 			ec = bcmd; 

-		} else Error(98);

+		} else Error(99);

 	}

 

 	static void TransferCmd(out TransferCmd! tc) {

@@ -1044,7 +1039,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 39) {

 			Get();

 			tc = new ReturnCmd(token); 

-		} else Error(99);

+		} else Error(100);

 		Expect(7);

 	}

 

@@ -1069,7 +1064,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				Get();

 				StmtList(out els);

 				elseOption = els; 

-			} else Error(100);

+			} else Error(101);

 		}

 		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); 

 	}

@@ -1128,7 +1123,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (StartOf(5)) {

 			Expression(out ee);

 			e = ee; 

-		} else Error(101);

+		} else Error(102);

 		Expect(9);

 	}

 

@@ -1166,7 +1161,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			}

 			Expect(7);

 			c = new AssignCmd(x, lhss, rhss); 

-		} else Error(102);

+		} else Error(103);

 	}

 

 	static void CallCmd(out Cmd! c) {

@@ -1229,7 +1224,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				}

 				Expect(9);

 				c = new CallCmd(x, first.val, es, ids); 

-			} else Error(103);

+			} else Error(104);

 		} else if (t.kind == 51) {

 			Get();

 			Ident(out first);

@@ -1283,7 +1278,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			}

 			Expect(9);

 			c = new CallCmd(x, first.val, es, ids); 

-		} else Error(104);

+		} else Error(105);

 	}

 

 	static void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) {

@@ -1323,7 +1318,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (StartOf(5)) {

 			Expression(out e);

 			exprOptional = e; 

-		} else Error(105);

+		} else Error(106);

 	}

 

 	static void CallOutIdent(out IToken id) {

@@ -1335,7 +1330,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 1) {

 			Ident(out p);

 			id = p; 

-		} else Error(106);

+		} else Error(107);

 	}

 

 	static void Expressions(out ExprSeq! es) {

@@ -1380,7 +1375,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 53) {

 			Get();

-		} else Error(107);

+		} else Error(108);

 	}

 

 	static void LogicalExpression(out Expr! e0) {

@@ -1418,7 +1413,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 55) {

 			Get();

-		} else Error(108);

+		} else Error(109);

 	}

 

 	static void ExpliesOp() {

@@ -1426,7 +1421,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 57) {

 			Get();

-		} else Error(109);

+		} else Error(110);

 	}

 

 	static void RelationalExpression(out Expr! e0) {

@@ -1444,7 +1439,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 59) {

 			Get();

-		} else Error(110);

+		} else Error(111);

 	}

 

 	static void OrOp() {

@@ -1452,7 +1447,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 61) {

 			Get();

-		} else Error(111);

+		} else Error(112);

 	}

 

 	static void BvTerm(out Expr! e0) {

@@ -1519,7 +1514,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			x = token; op=BinaryOperator.Opcode.Ge; 

 			break;

 		}

-		default: Error(112); break;

+		default: Error(113); break;

 		}

 	}

 

@@ -1551,7 +1546,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 72) {

 			Get();

 			x = token; op=BinaryOperator.Opcode.Sub; 

-		} else Error(113);

+		} else Error(114);

 	}

 

 	static void UnaryExpression(out Expr! e) {

@@ -1570,7 +1565,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); 

 		} else if (StartOf(12)) {

 			CoercionExpression(out e);

-		} else Error(114);

+		} else Error(115);

 	}

 

 	static void MulOp(out IToken! x, out BinaryOperator.Opcode op) {

@@ -1584,7 +1579,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 		} else if (t.kind == 74) {

 			Get();

 			x = token; op=BinaryOperator.Opcode.Mod; 

-		} else Error(115);

+		} else Error(116);

 	}

 

 	static void NegOp() {

@@ -1592,7 +1587,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			Get();

 		} else if (t.kind == 76) {

 			Get();

-		} else Error(116);

+		} else Error(117);

 	}

 

 	static void CoercionExpression(out Expr! e) {

@@ -1616,7 +1611,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				  e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);

 				}

 				

-			} else Error(117);

+			} else Error(118);

 		}

 	}

 

@@ -1726,7 +1721,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 					e = new NAryExpr(x, new FunctionCall(id), es); 

 				} else if (t.kind == 9) {

 					e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); 

-				} else Error(118);

+				} else Error(119);

 				Expect(9);

 			}

 			break;

@@ -1747,23 +1742,27 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 				if (e is BvBounds)

 				 SemErr("parentheses around bitvector bounds " +

 				        "are not allowed"); 

-			} else if (t.kind == 51 || t.kind == 80) {

+			} else if (t.kind == 51 || t.kind == 81) {

 				Forall();

 				x = token; 

 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

 				if (typeParams.Length + ds.Length > 0)

 				 e = new ForallExpr(x, typeParams, ds, kv, trig, e); 

-			} else if (t.kind == 81 || t.kind == 82) {

+			} else if (t.kind == 82 || t.kind == 83) {

 				Exists();

 				x = token; 

 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);

 				if (typeParams.Length + ds.Length > 0)

 				 e = new ExistsExpr(x, typeParams, ds, kv, trig, e); 

-			} else Error(119);

+			} else Error(120);

 			Expect(9);

 			break;

 		}

-		default: Error(120); break;

+		case 40: {

+			IfThenElseExpression(out e);

+			break;

+		}

+		default: Error(121); break;

 		}

 	}

 

@@ -1786,9 +1785,9 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 	static void Forall() {

 		if (t.kind == 51) {

 			Get();

-		} else if (t.kind == 80) {

+		} else if (t.kind == 81) {

 			Get();

-		} else Error(121);

+		} else Error(122);

 	}

 

 	static void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,

@@ -1805,7 +1804,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			}

 		} else if (t.kind == 1) {

 			BoundVars(q, out ds);

-		} else Error(122);

+		} else Error(123);

 		QSep();

 		while (t.kind == 25) {

 			AttributeOrTrigger(ref kv, ref trig);

@@ -1814,11 +1813,25 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 	}

 

 	static void Exists() {

-		if (t.kind == 81) {

+		if (t.kind == 82) {

 			Get();

-		} else if (t.kind == 82) {

+		} else if (t.kind == 83) {

 			Get();

-		} else Error(123);

+		} else Error(124);

+	}

+

+	static void IfThenElseExpression(out Expr! e) {

+		IToken! tok;

+		Expr! e0, e1, e2; 

+		e = dummyExpr; 

+		Expect(40);

+		tok = token; 

+		Expression(out e0);

+		Expect(80);

+		Expression(out e1);

+		Expect(41);

+		Expression(out e2);

+		e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); 

 	}

 

 	static void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {

@@ -1874,7 +1887,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			  trig.AddLast(new Trigger(tok, true, es, null));

 			}

 			

-		} else Error(124);

+		} else Error(125);

 		Expect(26);

 	}

 

@@ -1888,15 +1901,15 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 		} else if (StartOf(5)) {

 			Expression(out e);

 			o = e; 

-		} else Error(125);

+		} else Error(126);

 	}

 

 	static void QSep() {

-		if (t.kind == 83) {

+		if (t.kind == 84) {

 			Get();

-		} else if (t.kind == 84) {

+		} else if (t.kind == 85) {

 			Get();

-		} else Error(126);

+		} else Error(127);

 	}

 

 

@@ -1995,53 +2008,54 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 			case 77: s = "false expected"; break;

 			case 78: s = "true expected"; break;

 			case 79: s = "old expected"; break;

-			case 80: s = "\\u2200 expected"; break;

-			case 81: s = "exists expected"; break;

-			case 82: s = "\\u2203 expected"; break;

-			case 83: s = ":: expected"; break;

-			case 84: s = "\\u2022 expected"; break;

-			case 85: s = "??? expected"; break;

-			case 86: s = "invalid Function"; break;

+			case 80: s = "then expected"; break;

+			case 81: s = "\\u2200 expected"; break;

+			case 82: s = "exists expected"; break;

+			case 83: s = "\\u2203 expected"; break;

+			case 84: s = ":: expected"; break;

+			case 85: s = "\\u2022 expected"; break;

+			case 86: s = "??? expected"; break;

 			case 87: s = "invalid Function"; break;

-			case 88: s = "invalid Procedure"; break;

-			case 89: s = "invalid Type"; break;

-			case 90: s = "invalid TypeAtom"; break;

-			case 91: s = "invalid TypeArgs"; break;

-			case 92: s = "invalid Spec"; break;

-			case 93: s = "invalid SpecPrePost"; break;

+			case 88: s = "invalid Function"; break;

+			case 89: s = "invalid Procedure"; break;

+			case 90: s = "invalid Type"; break;

+			case 91: s = "invalid TypeAtom"; break;

+			case 92: s = "invalid TypeArgs"; break;

+			case 93: s = "invalid Spec"; break;

 			case 94: s = "invalid SpecPrePost"; break;

 			case 95: s = "invalid SpecPrePost"; break;

-			case 96: s = "invalid SpecBlock"; break;

-			case 97: s = "invalid LabelOrCmd"; break;

-			case 98: s = "invalid StructuredCmd"; break;

-			case 99: s = "invalid TransferCmd"; break;

-			case 100: s = "invalid IfCmd"; break;

-			case 101: s = "invalid Guard"; break;

-			case 102: s = "invalid LabelOrAssign"; break;

-			case 103: s = "invalid CallCmd"; break;

+			case 96: s = "invalid SpecPrePost"; break;

+			case 97: s = "invalid SpecBlock"; break;

+			case 98: s = "invalid LabelOrCmd"; break;

+			case 99: s = "invalid StructuredCmd"; break;

+			case 100: s = "invalid TransferCmd"; break;

+			case 101: s = "invalid IfCmd"; break;

+			case 102: s = "invalid Guard"; break;

+			case 103: s = "invalid LabelOrAssign"; break;

 			case 104: s = "invalid CallCmd"; break;

-			case 105: s = "invalid CallForallArg"; break;

-			case 106: s = "invalid CallOutIdent"; break;

-			case 107: s = "invalid EquivOp"; break;

-			case 108: s = "invalid ImpliesOp"; break;

-			case 109: s = "invalid ExpliesOp"; break;

-			case 110: s = "invalid AndOp"; break;

-			case 111: s = "invalid OrOp"; break;

-			case 112: s = "invalid RelOp"; break;

-			case 113: s = "invalid AddOp"; break;

-			case 114: s = "invalid UnaryExpression"; break;

-			case 115: s = "invalid MulOp"; break;

-			case 116: s = "invalid NegOp"; break;

-			case 117: s = "invalid CoercionExpression"; break;

-			case 118: s = "invalid AtomExpression"; break;

+			case 105: s = "invalid CallCmd"; break;

+			case 106: s = "invalid CallForallArg"; break;

+			case 107: s = "invalid CallOutIdent"; break;

+			case 108: s = "invalid EquivOp"; break;

+			case 109: s = "invalid ImpliesOp"; break;

+			case 110: s = "invalid ExpliesOp"; break;

+			case 111: s = "invalid AndOp"; break;

+			case 112: s = "invalid OrOp"; break;

+			case 113: s = "invalid RelOp"; break;

+			case 114: s = "invalid AddOp"; break;

+			case 115: s = "invalid UnaryExpression"; break;

+			case 116: s = "invalid MulOp"; break;

+			case 117: s = "invalid NegOp"; break;

+			case 118: s = "invalid CoercionExpression"; break;

 			case 119: s = "invalid AtomExpression"; break;

 			case 120: s = "invalid AtomExpression"; break;

-			case 121: s = "invalid Forall"; break;

-			case 122: s = "invalid QuantifierBody"; break;

-			case 123: s = "invalid Exists"; break;

-			case 124: s = "invalid AttributeOrTrigger"; break;

-			case 125: s = "invalid AttributeParameter"; break;

-			case 126: s = "invalid QSep"; break;

+			case 121: s = "invalid AtomExpression"; break;

+			case 122: s = "invalid Forall"; break;

+			case 123: s = "invalid QuantifierBody"; break;

+			case 124: s = "invalid Exists"; break;

+			case 125: s = "invalid AttributeOrTrigger"; break;

+			case 126: s = "invalid AttributeParameter"; break;

+			case 127: s = "invalid QSep"; break;

 

 			default: s = "error " + n; break;

 		}

@@ -2049,21 +2063,21 @@ out QKeyValue kv, out Trigger trig, out Expr! body) {
 	}

 

 	static bool[,]! set = {

-	{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-	{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-	{x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x},

-	{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-	{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x},

-	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},

-	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x},

-	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x},

-	{x,T,T,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x}

+	{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+	{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+	{x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x},

+	{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+	{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x},

+	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+	{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},

+	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x},

+	{x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x},

+	{x,T,T,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x}

 

 	};

 

diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc
index 745f8dc4..d8e18754 100644
--- a/Source/Core/Scanner.ssc
+++ b/Source/Core/Scanner.ssc
@@ -1,8 +1,3 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
 using System;

 using System.IO;

 using System.Collections;

@@ -350,7 +345,7 @@ public class Scanner {
 		start[8804] = 45;

 		start[8805] = 46;

 	}

-	const int noSym = 85;

+	const int noSym = 86;

 	static short[] start = new short[16385];

 

 

@@ -524,7 +519,8 @@ public class Scanner {
 			case "false": t.kind = 77; break;

 			case "true": t.kind = 78; break;

 			case "old": t.kind = 79; break;

-			case "exists": t.kind = 81; break;

+			case "then": t.kind = 80; break;

+			case "exists": t.kind = 82; break;

 			default: break;

 

     }

@@ -672,13 +668,13 @@ public class Scanner {
 			case 52:

 				{t.kind = 76; goto done;}

 			case 53:

-				{t.kind = 80; goto done;}

+				{t.kind = 81; goto done;}

 			case 54:

-				{t.kind = 82; goto done;}

-			case 55:

 				{t.kind = 83; goto done;}

-			case 56:

+			case 55:

 				{t.kind = 84; goto done;}

+			case 56:

+				{t.kind = 85; goto done;}

 			case 57: {t.kind = 0; goto done;}

     }

     done:

diff --git a/Source/Provers/Isabelle/Prover.ssc b/Source/Provers/Isabelle/Prover.ssc
index 9b91cd63..33764112 100644
--- a/Source/Provers/Isabelle/Prover.ssc
+++ b/Source/Provers/Isabelle/Prover.ssc
@@ -756,6 +756,12 @@ namespace Microsoft.Boogie.Isabelle
       b2i.Write(child2);

       return true;

     }

+

+    public bool VisitIfThenElseOp(VCExprNAry! node, B2I! b2i)

+    {

+      throw new System.NotImplementedException(); // TODO

+    }

+

     

     public bool VisitHeapSuccessionOp(VCExprNAry! node, B2I! b2i)

     {

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.ssc b/Source/Provers/SMTLib/SMTLibLineariser.ssc
index cbf69107..7efa109f 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.ssc
+++ b/Source/Provers/SMTLib/SMTLibLineariser.ssc
@@ -140,6 +140,7 @@ namespace Microsoft.Boogie.SMTLib
     internal const string! orName = "or"; // disjunction

     internal const string! notName = "not"; // negation

     internal const string! impliesName = "implies"; // implication

+    internal const string! iteName = "ite"; // if-then-else

     internal const string! iffName = "iff"; // logical equivalence

     internal const string! eqName = "="; // equality

     internal const string! lessName = "<";

@@ -160,6 +161,7 @@ namespace Microsoft.Boogie.SMTLib
     internal const string! boolNotName = "boolNot";

     internal const string! boolIffName = "boolIff";

     internal const string! boolImpliesName = "boolImplies";

+    internal const string! boolIteName = "ite";

     internal const string! termUEqual = "UEqual";

     internal const string! termTEqual = "TEqual";

     internal const string! termIntEqual = "IntEqual";

@@ -519,6 +521,11 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

+      public bool VisitIfThenElseOp  (VCExprNAry! node, LineariserOptions! options) {

+        WriteApplication(boolIteName, iteName, node, options);

+        return true;

+      }

+

       public bool VisitDistinctOp (VCExprNAry! node, LineariserOptions! options) {

         ExprLineariser.AssertAsFormula(distinctName, options);

         

diff --git a/Source/VCExpr/Boogie2VCExpr.ssc b/Source/VCExpr/Boogie2VCExpr.ssc
index f6393679..4698f541 100644
--- a/Source/VCExpr/Boogie2VCExpr.ssc
+++ b/Source/VCExpr/Boogie2VCExpr.ssc
@@ -738,6 +738,10 @@ namespace Microsoft.Boogie.VCExprAST
       return this.args[0];

     }

 

+    public VCExpr! Visit(IfThenElse! ite) {

+      return Gen.Function(VCExpressionGenerator.IfThenElseOp, this.args);

+    }

+

     ///////////////////////////////////////////////////////////////////////////////

 

     private VCExpr! TranslateBinaryOperator(BinaryOperator! app, List<VCExpr!>! args) {

diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc
index 52681162..7085bffe 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.ssc
+++ b/Source/VCExpr/SimplifyLikeLineariser.ssc
@@ -701,6 +701,19 @@ namespace Microsoft.Boogie.VCExprAST
         return true;

       }

 

+      public bool VisitIfThenElseOp (VCExprNAry! node, LineariserOptions! options) {

+        

+        wr.Write("(ITE ");

+        ExprLineariser.Linearise(node[0], options.SetAsTerm(false));

+        wr.Write(" ");

+        ExprLineariser.Linearise(node[1], options);

+        wr.Write(" ");

+        ExprLineariser.Linearise(node[2], options);

+        wr.Write(")");

+

+        return true;

+      }

+

       public bool VisitAddOp            (VCExprNAry! node, LineariserOptions! options) {

         if (CommandLineOptions.Clo.ReflectAdd) {

           WriteTermApplication(intAddNameReflect, node, options);

diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc
index 604be456..d41cb887 100644
--- a/Source/VCExpr/TypeErasure.ssc
+++ b/Source/VCExpr/TypeErasure.ssc
@@ -1016,6 +1016,17 @@ namespace Microsoft.Boogie.TypeErasure
       // (at least for Simplify ... should this be ensured at a later point?)

       return CastArguments(node, Type.Bool, bindings, Eraser.Polarity);

     }

+    public override VCExpr! VisitIfThenElseOp  (VCExprNAry! node, VariableBindings! bindings) {

+      List<VCExpr!>! newArgs = MutateSeq(node, bindings, 0);

+      newArgs[0] = AxBuilder.Cast(newArgs[0], Type.Bool);

+      Type t = node.Type;

+      if (!AxBuilder.UnchangedType(t)) {

+        t = AxBuilder.U;

+      }

+      newArgs[1] = AxBuilder.Cast(newArgs[1], t);

+      newArgs[2] = AxBuilder.Cast(newArgs[2], t);

+      return Gen.Function(node.Op, newArgs);

+    }

     public override VCExpr! VisitAddOp            (VCExprNAry! node, VariableBindings! bindings) {

       return CastArguments(node, Type.Int, bindings, 0);

     }

diff --git a/Source/VCExpr/VCExprAST.ssc b/Source/VCExpr/VCExprAST.ssc
index 5a9063cc..e08e6138 100644
--- a/Source/VCExpr/VCExprAST.ssc
+++ b/Source/VCExpr/VCExprAST.ssc
@@ -221,6 +221,7 @@ namespace Microsoft.Boogie
     // ternary version of the subtype operator, the first argument of which gives

     // the type of the compared terms

     public static readonly VCExprOp! Subtype3Op       = new VCExprNAryOp (3, Type.Bool);

+    public static readonly VCExprOp! IfThenElseOp     = new VCExprIfThenElseOp();

 

     public VCExprOp! BoogieFunctionOp(Function! func) {

       return new VCExprBoogieFunctionOp(func);

@@ -990,6 +991,34 @@ namespace Microsoft.Boogie.VCExprAST
     }

   }

 

+  public class VCExprIfThenElseOp : VCExprOp {

+    public override int Arity { get { return 3; } }

+    public override int TypeParamArity { get { return 0; } }

+    public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {

+      return args[1].Type;

+    }

+

+    [Pure][Reads(ReadsAttribute.Reads.Nothing)]

+    public override bool Equals(object that) {

+      if (Object.ReferenceEquals(this, that))

+        return true;

+      if (that is VCExprIfThenElseOp)

+        return true;

+      return false;

+    }

+    [Pure]

+    public override int GetHashCode() {

+      return 1;

+    }

+

+    internal VCExprIfThenElseOp() {

+    }

+    public override Result Accept<Result, Arg>

+           (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {

+      return visitor.VisitIfThenElseOp(expr, arg);

+    }

+  }

+

   /////////////////////////////////////////////////////////////////////////////////

   // Bitvector operators

 

diff --git a/Source/VCExpr/VCExprASTPrinter.ssc b/Source/VCExpr/VCExprASTPrinter.ssc
index 1c143516..ca8ec11a 100644
--- a/Source/VCExpr/VCExprASTPrinter.ssc
+++ b/Source/VCExpr/VCExprASTPrinter.ssc
@@ -193,6 +193,9 @@ namespace Microsoft.Boogie.VCExprAST
     public bool VisitBvConcatOp (VCExprNAry! node, TextWriter! wr) {

       return PrintNAry("BvConcat", node, wr);

     }

+    public bool VisitIfThenElseOp(VCExprNAry! node, TextWriter! wr) {

+      return PrintNAry("if-then-else", node, wr);

+    }

     public bool VisitAddOp            (VCExprNAry! node, TextWriter! wr) {

       if (CommandLineOptions.Clo.ReflectAdd) {

         return PrintNAry("Reflect$Add", node, wr);

@@ -237,4 +240,4 @@ namespace Microsoft.Boogie.VCExprAST
   }

 

 

-}
\ No newline at end of file
+}

diff --git a/Source/VCExpr/VCExprASTVisitors.ssc b/Source/VCExpr/VCExprASTVisitors.ssc
index 2808f6bb..1ae71b26 100644
--- a/Source/VCExpr/VCExprASTVisitors.ssc
+++ b/Source/VCExpr/VCExprASTVisitors.ssc
@@ -51,6 +51,7 @@ namespace Microsoft.Boogie.VCExprAST
     Result VisitSubtypeOp        (VCExprNAry! node, Arg arg);

     Result VisitSubtype3Op       (VCExprNAry! node, Arg arg);

     Result VisitBoogieFunctionOp (VCExprNAry! node, Arg arg);

+    Result VisitIfThenElseOp     (VCExprNAry! node, Arg arg);

   }

 

   //////////////////////////////////////////////////////////////////////////////

@@ -955,6 +956,9 @@ namespace Microsoft.Boogie.VCExprAST
     public virtual Result VisitBvConcatOp (VCExprNAry! node, Arg arg) {

       return StandardResult(node, arg);

     }

+    public virtual Result VisitIfThenElseOp (VCExprNAry! node, Arg arg) {

+      return StandardResult(node, arg);

+    }

     public virtual Result VisitAddOp            (VCExprNAry! node, Arg arg) {

       return StandardResult(node, arg);

     }

diff --git a/Test/test1/Answer b/Test/test1/Answer
index b0f4aac3..10ad5494 100644
--- a/Test/test1/Answer
+++ b/Test/test1/Answer
@@ -135,3 +135,7 @@ FunBody.bpl(6,45): Error: function body with invalid type: bool (expected: int)
 FunBody.bpl(8,61): Error: function body with invalid type: int (expected: alpha)

 FunBody.bpl(10,58): Error: function body with invalid type: int (expected: alpha)

 3 type checking errors detected in FunBody.bpl

+IfThenElse0.bpl(5,7): Error: the first argument to if-then-else should be bool, not int

+IfThenElse0.bpl(6,7): Error: branches of if-then-else have incompatible types bool and int

+IfThenElse0.bpl(7,2): Error: mismatched types in assignment command (cannot assign int to bool)

+3 type checking errors detected in IfThenElse0.bpl

diff --git a/Test/test1/IfThenElse0.bpl b/Test/test1/IfThenElse0.bpl
new file mode 100644
index 00000000..c26461b1
--- /dev/null
+++ b/Test/test1/IfThenElse0.bpl
@@ -0,0 +1,8 @@
+procedure foo()
+{
+  var b:bool, i:int;
+
+  b := if i then b else b;
+  b := if b then b else i;
+  b := if b then i else i;
+}
diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat
index c6881263..dda3a0af 100644
--- a/Test/test1/runtest.bat
+++ b/Test/test1/runtest.bat
@@ -17,3 +17,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe
 %BGEXE% %* /noVerify Orderings.bpl

 %BGEXE% %* /noVerify EmptyCallArgs.bpl

 %BGEXE% %* /noVerify FunBody.bpl

+%BGEXE% %* /noVerify IfThenElse0.bpl

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 1e5a0d5f..230a8861 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -323,6 +323,16 @@ Execution trace:
     Implies.bpl(11,3): anon0

 

 Boogie program verifier finished with 0 verified, 2 errors

+

+-------------------- IfThenElse1.bpl --------------------

+IfThenElse1.bpl(26,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    IfThenElse1.bpl(26,3): anon0

+IfThenElse1.bpl(33,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    IfThenElse1.bpl(33,3): anon0

+

+Boogie program verifier finished with 2 verified, 2 errors

 -------------------- sk_hack.bpl --------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/test2/IfThenElse1.bpl b/Test/test2/IfThenElse1.bpl
new file mode 100644
index 00000000..8a867f50
--- /dev/null
+++ b/Test/test2/IfThenElse1.bpl
@@ -0,0 +1,34 @@
+type t1;
+
+procedure ok()
+{
+  var b:bool, x:int, y:int;
+
+  assert x == if b then x else x;
+  assert x == if true then x else y;
+}
+
+procedure ok2()
+{
+  var x:int, y:int;
+  var a:t1, b:t1, c:t1;
+
+  c := if x > y then a else b;
+  assert c == a || c == b;
+  assume x > y;
+  assert c == a;
+}
+
+procedure fail1()
+{
+  var b:bool, x:int, y:int;
+
+  assert x == if b then x else y;
+}
+
+procedure fail2()
+{
+  var b:bool, x:int, y:int;
+
+  assert x == if false then x else y;
+}
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index 5f48a799..ab9ec103 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -10,7 +10,8 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
             CutBackEdge.bpl False.bpl LoopInvAssume.bpl

             strings-no-where.bpl strings-where.bpl

             Structured.bpl Where.bpl UpdateExpr.bpl

-            NeverPattern.bpl NullaryMaps.bpl Implies.bpl) do (

+            NeverPattern.bpl NullaryMaps.bpl Implies.bpl

+	    IfThenElse1.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /noinfer %%f