Change the return type of StandardVisitor.VisitForAllExpr() from

ForAllExpr to Expr. Enforcing the return type be ForAllExpr 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.
a visitor that does constant folding of an Expr tree

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index d53a75a4..f261553b 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -461,7 +461,7 @@ namespace Microsoft.Boogie.VCExprAST {
       return node;

     }

 

-    public override ForallExpr VisitForallExpr(ForallExpr node) {

+    public override Expr VisitForallExpr(ForallExpr node) {

       //Contract.Requires(node != null);

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

       node = (ForallExpr)this.VisitQuantifierExpr(node);