Fix duplicator so that BVConcatExpr and BVExtractExpr are handled. Patch by Daniel Liew.

1 files changed, 8 insertions, 0 deletions

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index cd084e14..70018a1a 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -71,6 +71,14 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Block>() != null);

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

     }

+    public override BvConcatExpr VisitBvConcatExpr (BvConcatExpr node) {

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

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

+    }

+    public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {

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

+      return base.VisitBvExtractExpr((BvExtractExpr) node.Clone());

+    }

     public override Expr VisitCodeExpr(CodeExpr node) {

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

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