mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #7084

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-15 08:49:10 -08:00
parent 91ca55e5ad
commit 4ff352fcac
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -615,6 +615,8 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
if (m_blast_quant) { if (m_blast_quant) {
if (m_bindings.empty()) if (m_bindings.empty())
return false; return false;
if (!butil().is_bv(t))
return false;
unsigned shift = m_shifts.back(); unsigned shift = m_shifts.back();
if (t->get_idx() >= m_bindings.size()) { if (t->get_idx() >= m_bindings.size()) {
if (shift == 0) if (shift == 0)