Modified internal abstract float representation to allow user-defined mantissa and exponent

1 files changed, 6 insertions, 0 deletions

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 0323d4db..97215cfb 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -103,6 +103,12 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Type>() != null);

       return this.VisitType(node);

     }

+    public virtual Type VisitFloatType(FloatType node)

+    {

+      Contract.Requires(node != null);

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

+      return this.VisitType(node);

+    }

     public virtual Expr VisitBvConcatExpr(BvConcatExpr node) {

       Contract.Requires(node != null);

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