From 6eebfd06296a39c3aeabe555797f70ac8bb0e110 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 8 Apr 2020 18:10:12 -0700
Subject: [PATCH] fix #3880

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bv_trailing.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp
index e06f5eeb2..da962b729 100644
--- a/src/ast/rewriter/bv_trailing.cpp
+++ b/src/ast/rewriter/bv_trailing.cpp
@@ -168,7 +168,6 @@ struct bv_trailing::imp {
         case 1: result = new_args.get(0); break;
         default: result = m.mk_app(m_util.get_fid(), OP_BMUL, new_args.size(), new_args.c_ptr());
         }
-        SASSERT(retv == m_util.get_bv_size(result));
         return retv;
     }