mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

Fix bv2int_translator assertion: extend early-return for non-basic bool non-BV expressions in plugin mode

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-13 04:54:48 +00:00 • committed by GitHub
parent 88d0d282d6
commit f662eed78d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/bv2int_translator.cpp
View file

@ -90,7 +90,7 @@ void bv2int_translator::translate_expr(expr* e) {
translate_var(to_var(e));
else {
app* ap = to_app(e);
if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) {
if (m_is_plugin && m.is_bool(ap) && ap->get_family_id() != bv.get_family_id()) {
set_translated(e, e);
return;
}