From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 23:14:18 -0600
Subject: Merging complete.  Everything looks good *crosses fingers*

---
 Source/VCExpr/VCExprASTPrinter.cs | 864 +++++++++++++++++++-------------------
 1 file changed, 432 insertions(+), 432 deletions(-)

(limited to 'Source/VCExpr/VCExprASTPrinter.cs')

diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index 8e2f5d12..dac9604c 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -1,432 +1,432 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation.  All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Text;
-using System.IO;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using Microsoft.Basetypes;
-
-// A simple visitor for turning a VCExpr into a human-readable string
-// (S-expr syntax)
-
-namespace Microsoft.Boogie.VCExprAST {
-
-  public class VCExprPrinter : IVCExprVisitor<bool, TextWriter/*!*/> {
-    private VCExprOpPrinter OpPrinterVar = null;
-    private VCExprOpPrinter/*!*/ OpPrinter {
-      get {
-        Contract.Ensures(Contract.Result<VCExprOpPrinter>() != null);
-
-        if (OpPrinterVar == null)
-          OpPrinterVar = new VCExprOpPrinter(this);
-        return OpPrinterVar;
-      }
-    }
-
-    public void Print(VCExpr expr, TextWriter wr) {
-      Contract.Requires(wr != null);
-      Contract.Requires(expr != null);
-      expr.Accept<bool, TextWriter/*!*/>(this, wr);
-    }
-
-    public bool Visit(VCExprLiteral node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      if (node == VCExpressionGenerator.True) {
-        wr.Write("true");
-      } else if (node == VCExpressionGenerator.False) {
-        wr.Write("false");
-      } else if (node is VCExprIntLit) {
-        wr.Write(((VCExprIntLit)node).Val);
-      } else {
-        Contract.Assert(false);
-        throw new cce.UnreachableException();
-      }
-      return true;
-    }
-    public bool Visit(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      VCExprOp/*!*/ op = node.Op;
-      Contract.Assert(op != null);
-
-      if (op.Equals(VCExpressionGenerator.AndOp) ||
-          op.Equals(VCExpressionGenerator.OrOp)) {
-        // handle these operators without recursion
-
-        wr.Write("({0}",
-                 op.Equals(VCExpressionGenerator.AndOp) ? "And" : "Or");
-        IEnumerator/*!*/ enumerator = new VCExprNAryUniformOpEnumerator(node);
-        Contract.Assert(enumerator != null);
-        while (enumerator.MoveNext()) {
-          VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
-          if (naryExpr == null || !naryExpr.Op.Equals(op)) {
-            wr.Write(" ");
-            Print(cce.NonNull((VCExpr/*!*/)enumerator.Current), wr);
-          }
-        }
-
-        wr.Write(")");
-
-        return true;
-      }
-
-      return node.Accept<bool, TextWriter/*!*/>(OpPrinter, wr);
-    }
-    public bool Visit(VCExprVar node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      wr.Write(node.Name);
-      return true;
-    }
-    public bool Visit(VCExprQuantifier node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      string/*!*/ quan = node.Quan == Quantifier.ALL ? "Forall" : "Exists";
-      Contract.Assert(quan != null);
-
-      wr.Write("({0} ", quan);
-
-      if (node.TypeParameters.Count > 0) {
-        wr.Write("<");
-        string/*!*/ sep = "";
-        foreach (TypeVariable/*!*/ v in node.TypeParameters) {
-          Contract.Assert(v != null);
-          wr.Write(sep);
-          sep = ", ";
-          wr.Write("{0}", v.Name);
-        }
-        wr.Write("> ");
-      }
-
-      if (node.BoundVars.Count > 0) {
-        string/*!*/ sep = "";
-        foreach (VCExprVar/*!*/ v in node.BoundVars) {
-          Contract.Assert(v != null);
-          wr.Write(sep);
-          sep = ", ";
-          Print(v, wr);
-        }
-        wr.Write(" ");
-      }
-
-      wr.Write(":: ");
-
-      if (node.Triggers.Count > 0) {
-        wr.Write("{0} ", "{");
-        string/*!*/ sep = "";
-        foreach (VCTrigger/*!*/ t in node.Triggers) {
-          Contract.Assert(t != null);
-          wr.Write(sep);
-          sep = ", ";
-          string/*!*/ sep2 = "";
-          foreach (VCExpr/*!*/ e in t.Exprs) {
-            Contract.Assert(e != null);
-            wr.Write(sep2);
-            sep2 = "+";
-            Print(e, wr);
-          }
-        }
-        wr.Write(" {0} ", "}");
-      }
-
-      Print(node.Body, wr);
-      wr.Write(")");
-      return true;
-    }
-    public bool Visit(VCExprLet node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      wr.Write("(Let ");
-
-      string/*!*/ sep = "";
-      foreach (VCExprLetBinding/*!*/ b in node) {
-        Contract.Assert(b != null);
-        wr.Write(sep);
-        sep = ", ";
-        Print(b.V, wr);
-        wr.Write(" = ");
-        Print(b.E, wr);
-      }
-      wr.Write(" ");
-
-      Print(node.Body, wr);
-      wr.Write(")");
-      return true;
-    }
-  }
-
-  public class VCExprOpPrinter : IVCExprOpVisitor<bool, TextWriter/*!*/> {
-    private VCExprPrinter/*!*/ ExprPrinter;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(ExprPrinter != null);
-    }
-
-
-    public VCExprOpPrinter(VCExprPrinter exprPrinter) {
-      Contract.Requires(exprPrinter != null);
-      this.ExprPrinter = exprPrinter;
-    }
-
-    private bool PrintNAry(string op, VCExprNAry node, TextWriter wr) {
-      Contract.Requires(wr != null);
-      Contract.Requires(node != null);
-      Contract.Requires(op != null);
-      wr.Write("({0}", op);
-      foreach (VCExpr/*!*/ arg in node) {
-        Contract.Assert(arg != null);
-        wr.Write(" ");
-        ExprPrinter.Print(arg, wr);
-      }
-      wr.Write(")");
-      return true;
-    }
-
-    public bool VisitNotOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("!", node, wr);
-    }
-    public bool VisitEqOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("==", node, wr);
-    }
-    public bool VisitNeqOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("!=", node, wr);
-    }
-    public bool VisitAndOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      Contract.Assert(false);
-      throw new cce.UnreachableException();
-    }
-    public bool VisitOrOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      Contract.Assert(false);
-      throw new cce.UnreachableException();
-    }
-    public bool VisitImpliesOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("Implies", node, wr);
-    }
-    public bool VisitDistinctOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("Distinct", node, wr);
-    }
-    public bool VisitLabelOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      VCExprLabelOp/*!*/ op = (VCExprLabelOp)node.Op;
-      Contract.Assert(op != null);
-      return PrintNAry("Label " + op.label, node, wr);
-    }
-    public bool VisitSelectOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("Select", node, wr);
-    }
-    public bool VisitStoreOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("Store", node, wr);
-    }
-    public bool VisitFloatAddOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.add", node, wr);
-    }
-    public bool VisitFloatSubOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.sub", node, wr);
-    }
-    public bool VisitFloatMulOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.mul", node, wr);
-    }
-    public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.div", node, wr);
-    }
-    public bool VisitFloatRemOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.rem", node, wr);
-    }
-    public bool VisitFloatMinOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.min", node, wr);
-    }
-    public bool VisitFloatMaxOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.max", node, wr);
-    }
-    public bool VisitFloatLeqOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.leq", node, wr);
-    }
-    public bool VisitFloatLtOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.lt", node, wr);
-    }
-    public bool VisitFloatGeqOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.geq", node, wr);
-    }
-    public bool VisitFloatGtOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.gt", node, wr);
-    }
-    public bool VisitFloatEqOp(VCExprNAry node, TextWriter wr)
-    {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("fp.eq", node, wr);
-    }
-    public bool VisitBvOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("Bv", node, wr);
-    }
-    public bool VisitBvExtractOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("BvExtract", node, wr);
-    }
-    public bool VisitBvConcatOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("BvConcat", node, wr);
-    }
-    public bool VisitIfThenElseOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("if-then-else", node, wr);
-    }
-    public bool VisitCustomOp(VCExprNAry/*!*/ node, TextWriter/*!*/ wr) {
-      //Contract.Requires(node!=null);
-      //Contract.Requires(wr != null);
-      VCExprCustomOp op = (VCExprCustomOp)node.Op;
-      return PrintNAry(op.Name, node, wr);
-    }
-    public bool VisitAddOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      if (CommandLineOptions.Clo.ReflectAdd) {
-        return PrintNAry("Reflect$Add", node, wr);
-      } else {
-        return PrintNAry("+", node, wr);
-      }
-    }
-    public bool VisitSubOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("-", node, wr);
-    }
-    public bool VisitMulOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("*", node, wr);
-    }
-    public bool VisitDivOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("div", node, wr);
-    }
-    public bool VisitModOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("mod", node, wr);
-    }
-    public bool VisitRealDivOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("/", node, wr);
-    }
-    public bool VisitPowOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("**", node, wr);
-    }
-    public bool VisitLtOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("<", node, wr);
-    }
-    public bool VisitLeOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("<=", node, wr);
-    }
-    public bool VisitGtOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry(">", node, wr);
-    }
-    public bool VisitGeOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry(">=", node, wr);
-    }
-    public bool VisitSubtypeOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("<:", node, wr);
-    }
-    public bool VisitSubtype3Op(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("<::", node, wr);
-    }
-    public bool VisitToIntOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("int", node, wr);
-    }
-    public bool VisitToRealOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      return PrintNAry("real", node, wr);
-    }
-    public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {
-      //Contract.Requires(wr != null);
-      //Contract.Requires(node != null);
-      VCExprBoogieFunctionOp/*!*/ op = (VCExprBoogieFunctionOp)node.Op;
-      Contract.Assert(op != null);
-      return PrintNAry(op.Func.Name, node, wr);
-    }
-  }
-
-
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+
+// A simple visitor for turning a VCExpr into a human-readable string
+// (S-expr syntax)
+
+namespace Microsoft.Boogie.VCExprAST {
+
+  public class VCExprPrinter : IVCExprVisitor<bool, TextWriter/*!*/> {
+    private VCExprOpPrinter OpPrinterVar = null;
+    private VCExprOpPrinter/*!*/ OpPrinter {
+      get {
+        Contract.Ensures(Contract.Result<VCExprOpPrinter>() != null);
+
+        if (OpPrinterVar == null)
+          OpPrinterVar = new VCExprOpPrinter(this);
+        return OpPrinterVar;
+      }
+    }
+
+    public void Print(VCExpr expr, TextWriter wr) {
+      Contract.Requires(wr != null);
+      Contract.Requires(expr != null);
+      expr.Accept<bool, TextWriter/*!*/>(this, wr);
+    }
+
+    public bool Visit(VCExprLiteral node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      if (node == VCExpressionGenerator.True) {
+        wr.Write("true");
+      } else if (node == VCExpressionGenerator.False) {
+        wr.Write("false");
+      } else if (node is VCExprIntLit) {
+        wr.Write(((VCExprIntLit)node).Val);
+      } else {
+        Contract.Assert(false);
+        throw new cce.UnreachableException();
+      }
+      return true;
+    }
+    public bool Visit(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      VCExprOp/*!*/ op = node.Op;
+      Contract.Assert(op != null);
+
+      if (op.Equals(VCExpressionGenerator.AndOp) ||
+          op.Equals(VCExpressionGenerator.OrOp)) {
+        // handle these operators without recursion
+
+        wr.Write("({0}",
+                 op.Equals(VCExpressionGenerator.AndOp) ? "And" : "Or");
+        IEnumerator/*!*/ enumerator = new VCExprNAryUniformOpEnumerator(node);
+        Contract.Assert(enumerator != null);
+        while (enumerator.MoveNext()) {
+          VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+          if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+            wr.Write(" ");
+            Print(cce.NonNull((VCExpr/*!*/)enumerator.Current), wr);
+          }
+        }
+
+        wr.Write(")");
+
+        return true;
+      }
+
+      return node.Accept<bool, TextWriter/*!*/>(OpPrinter, wr);
+    }
+    public bool Visit(VCExprVar node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      wr.Write(node.Name);
+      return true;
+    }
+    public bool Visit(VCExprQuantifier node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      string/*!*/ quan = node.Quan == Quantifier.ALL ? "Forall" : "Exists";
+      Contract.Assert(quan != null);
+
+      wr.Write("({0} ", quan);
+
+      if (node.TypeParameters.Count > 0) {
+        wr.Write("<");
+        string/*!*/ sep = "";
+        foreach (TypeVariable/*!*/ v in node.TypeParameters) {
+          Contract.Assert(v != null);
+          wr.Write(sep);
+          sep = ", ";
+          wr.Write("{0}", v.Name);
+        }
+        wr.Write("> ");
+      }
+
+      if (node.BoundVars.Count > 0) {
+        string/*!*/ sep = "";
+        foreach (VCExprVar/*!*/ v in node.BoundVars) {
+          Contract.Assert(v != null);
+          wr.Write(sep);
+          sep = ", ";
+          Print(v, wr);
+        }
+        wr.Write(" ");
+      }
+
+      wr.Write(":: ");
+
+      if (node.Triggers.Count > 0) {
+        wr.Write("{0} ", "{");
+        string/*!*/ sep = "";
+        foreach (VCTrigger/*!*/ t in node.Triggers) {
+          Contract.Assert(t != null);
+          wr.Write(sep);
+          sep = ", ";
+          string/*!*/ sep2 = "";
+          foreach (VCExpr/*!*/ e in t.Exprs) {
+            Contract.Assert(e != null);
+            wr.Write(sep2);
+            sep2 = "+";
+            Print(e, wr);
+          }
+        }
+        wr.Write(" {0} ", "}");
+      }
+
+      Print(node.Body, wr);
+      wr.Write(")");
+      return true;
+    }
+    public bool Visit(VCExprLet node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      wr.Write("(Let ");
+
+      string/*!*/ sep = "";
+      foreach (VCExprLetBinding/*!*/ b in node) {
+        Contract.Assert(b != null);
+        wr.Write(sep);
+        sep = ", ";
+        Print(b.V, wr);
+        wr.Write(" = ");
+        Print(b.E, wr);
+      }
+      wr.Write(" ");
+
+      Print(node.Body, wr);
+      wr.Write(")");
+      return true;
+    }
+  }
+
+  public class VCExprOpPrinter : IVCExprOpVisitor<bool, TextWriter/*!*/> {
+    private VCExprPrinter/*!*/ ExprPrinter;
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(ExprPrinter != null);
+    }
+
+
+    public VCExprOpPrinter(VCExprPrinter exprPrinter) {
+      Contract.Requires(exprPrinter != null);
+      this.ExprPrinter = exprPrinter;
+    }
+
+    private bool PrintNAry(string op, VCExprNAry node, TextWriter wr) {
+      Contract.Requires(wr != null);
+      Contract.Requires(node != null);
+      Contract.Requires(op != null);
+      wr.Write("({0}", op);
+      foreach (VCExpr/*!*/ arg in node) {
+        Contract.Assert(arg != null);
+        wr.Write(" ");
+        ExprPrinter.Print(arg, wr);
+      }
+      wr.Write(")");
+      return true;
+    }
+
+    public bool VisitNotOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("!", node, wr);
+    }
+    public bool VisitEqOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("==", node, wr);
+    }
+    public bool VisitNeqOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("!=", node, wr);
+    }
+    public bool VisitAndOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      Contract.Assert(false);
+      throw new cce.UnreachableException();
+    }
+    public bool VisitOrOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      Contract.Assert(false);
+      throw new cce.UnreachableException();
+    }
+    public bool VisitImpliesOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("Implies", node, wr);
+    }
+    public bool VisitDistinctOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("Distinct", node, wr);
+    }
+    public bool VisitLabelOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      VCExprLabelOp/*!*/ op = (VCExprLabelOp)node.Op;
+      Contract.Assert(op != null);
+      return PrintNAry("Label " + op.label, node, wr);
+    }
+    public bool VisitSelectOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("Select", node, wr);
+    }
+    public bool VisitStoreOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("Store", node, wr);
+    }
+    public bool VisitFloatAddOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.add", node, wr);
+    }
+    public bool VisitFloatSubOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.sub", node, wr);
+    }
+    public bool VisitFloatMulOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.mul", node, wr);
+    }
+    public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.div", node, wr);
+    }
+    public bool VisitFloatRemOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.rem", node, wr);
+    }
+    public bool VisitFloatMinOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.min", node, wr);
+    }
+    public bool VisitFloatMaxOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.max", node, wr);
+    }
+    public bool VisitFloatLeqOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.leq", node, wr);
+    }
+    public bool VisitFloatLtOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.lt", node, wr);
+    }
+    public bool VisitFloatGeqOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.geq", node, wr);
+    }
+    public bool VisitFloatGtOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.gt", node, wr);
+    }
+    public bool VisitFloatEqOp(VCExprNAry node, TextWriter wr)
+    {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("fp.eq", node, wr);
+    }
+    public bool VisitBvOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("Bv", node, wr);
+    }
+    public bool VisitBvExtractOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("BvExtract", node, wr);
+    }
+    public bool VisitBvConcatOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("BvConcat", node, wr);
+    }
+    public bool VisitIfThenElseOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("if-then-else", node, wr);
+    }
+    public bool VisitCustomOp(VCExprNAry/*!*/ node, TextWriter/*!*/ wr) {
+      //Contract.Requires(node!=null);
+      //Contract.Requires(wr != null);
+      VCExprCustomOp op = (VCExprCustomOp)node.Op;
+      return PrintNAry(op.Name, node, wr);
+    }
+    public bool VisitAddOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      if (CommandLineOptions.Clo.ReflectAdd) {
+        return PrintNAry("Reflect$Add", node, wr);
+      } else {
+        return PrintNAry("+", node, wr);
+      }
+    }
+    public bool VisitSubOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("-", node, wr);
+    }
+    public bool VisitMulOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("*", node, wr);
+    }
+    public bool VisitDivOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("div", node, wr);
+    }
+    public bool VisitModOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("mod", node, wr);
+    }
+    public bool VisitRealDivOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("/", node, wr);
+    }
+    public bool VisitPowOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("**", node, wr);
+    }
+    public bool VisitLtOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("<", node, wr);
+    }
+    public bool VisitLeOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("<=", node, wr);
+    }
+    public bool VisitGtOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry(">", node, wr);
+    }
+    public bool VisitGeOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry(">=", node, wr);
+    }
+    public bool VisitSubtypeOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("<:", node, wr);
+    }
+    public bool VisitSubtype3Op(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("<::", node, wr);
+    }
+    public bool VisitToIntOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("int", node, wr);
+    }
+    public bool VisitToRealOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      return PrintNAry("real", node, wr);
+    }
+    public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {
+      //Contract.Requires(wr != null);
+      //Contract.Requires(node != null);
+      VCExprBoogieFunctionOp/*!*/ op = (VCExprBoogieFunctionOp)node.Op;
+      Contract.Assert(op != null);
+      return PrintNAry(op.Func.Name, node, wr);
+    }
+  }
+
+
+}
-- 
cgit v1.2.3