Change the return type of StandardVisitor.VisitBvConcatExpr() from

BvConcatExpr to Expr. Enforcing the return type be BvConcatExpr is
too restrictive. For example it prevents anyone from implementing
a visitor that does constant folding of an Expr tree.

There is precedence for this. For example VisitNAryExpr() returns
an Expr not an NAryExpr.

Unfortunately this a breaking API change so anyone who subclasses
the StandardVisitor (or one of its sub classes) and overrides this
method will get compilation errors until they change the return type.

2 files changed, 3 insertions, 3 deletions

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 32eb2480..fbe36feb 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -77,7 +77,7 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Block>() != null);

       return base.VisitBlock((Block) node.Clone());

     }

-    public override BvConcatExpr VisitBvConcatExpr (BvConcatExpr node) {

+    public override Expr VisitBvConcatExpr (BvConcatExpr node) {

       Contract.Ensures(Contract.Result<BvConcatExpr>() != null);

       return base.VisitBvConcatExpr((BvConcatExpr) node.Clone());

     }

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index f7538b53..4c167953 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -103,7 +103,7 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Type>() != null);

       return this.VisitType(node);

     }

-    public virtual BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {

+    public virtual Expr VisitBvConcatExpr(BvConcatExpr node) {

       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<BvConcatExpr>() != null);

       node.E0 = this.VisitExpr(node.E0);

@@ -679,7 +679,7 @@ namespace Microsoft.Boogie {
           Contract.Ensures(Contract.Result<Type>() == node);

           return this.VisitType(node);

       }

-      public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node)

+      public override Expr VisitBvConcatExpr(BvConcatExpr node)

       {

           Contract.Ensures(Contract.Result<BvConcatExpr>() == node);

           this.VisitExpr(node.E0);