From 4ff352fcace8880e3607f643683ca6e9c88c87fd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Jan 2024 08:49:10 -0800 Subject: [PATCH] fix #7084 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 68e3825c9..bb8b067e8 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -615,6 +615,8 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); if (m_blast_quant) { if (m_bindings.empty()) return false; + if (!butil().is_bv(t)) + return false; unsigned shift = m_shifts.back(); if (t->get_idx() >= m_bindings.size()) { if (shift == 0)