mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-16 03:55:42 +00:00
Code Activity

Model extraction bug

Browse source
This commit is contained in:
CEisenhofer 2026-07-15 17:10:51 +02:00
parent 325cff40da
commit 96241a5025
1 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/seq/seq_nielsen.cpp
View file

@ -6339,7 +6339,14 @@ namespace seq {
for (auto const& mem : node.str_mems()) {
if (!mem.is_primitive())
continue;
if (mem.m_str->first() != var)
// Compare by expression, not snode pointer: the sgraph may hold
// several distinct snode objects for the same hash-consed
// expression (seq_model passes a snode re-created from the
// substitution tree). A pointer mismatch would silently drop the
// variable's view/plain components here, and product_witness's
// empty-tuple fast path would then fabricate an unconstrained
// filler word resulting in an invalid model.
if (mem.m_str->first()->get_expr() != var->get_expr())
continue;
switch (mem.m_kind) {
case mem_kind::plain: