From fb397cbe25f9e20c541ba0880e0c4b2c2f05bce5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 4 Jan 2019 08:18:40 -0800 Subject: [PATCH] remove incorrect assertion Signed-off-by: Nikolaj Bjorner --- src/smt/theory_bv.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 711c15a33..8db1df26b 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -81,8 +81,6 @@ namespace smt { TRACE("bv", tout << "bit2bool: " << mk_pp(n, ctx.get_manager()) << "\n";); expr* first_arg = n->get_arg(0); - SASSERT(!m_util.is_numeral(first_arg)); - if (!ctx.e_internalized(first_arg)) { // This may happen if bit2bool(x) is in a conflict // clause that is being reinitialized, and x was not reinitialized