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

Analysis of ASSERTION VIOLATION in qe_mbp.cpp - root cause identified

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-13 00:33:39 +00:00 • committed by GitHub
parent f5d3417c4f
commit 535bafc6d0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3704 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/qe/qe_mbp.cpp
View file

@ -562,11 +562,15 @@ public:
arith_util ari_u(m);
datatype_util dt_u(m);
IF_VERBOSE(2, verbose_stream() << "spacer_qel start: fml=" << fml << " vars=" << vars << "\n");
do_qel(vars, fml);
IF_VERBOSE(2, verbose_stream() << "spacer_qel after do_qel: fml=" << fml << " vars=" << vars << "\n");
qel_project(vars, mdl, fml, m_reduce_all_selects);
IF_VERBOSE(2, verbose_stream() << "spacer_qel after qel_project: fml=" << fml << " vars=" << vars << "\n");
flatten_and(fml);
m_rw(fml);
rewrite_as_const_arr(fml, mdl, fml);
IF_VERBOSE(2, verbose_stream() << "spacer_qel after rewrite: fml=" << fml << " eval=" << eval(fml) << "\n");
for (app* v : vars) {
SASSERT(!arr_u.is_array(v) && !dt_u.is_datatype(v->get_sort()));
@ -604,6 +608,7 @@ public:
other_vars.reset();
}
IF_VERBOSE(1, if (eval.is_false(fml)) verbose_stream() << "DEBUG spacer_qel fml=" << fml << "\n";);
SASSERT(!eval.is_false(fml));
vars.reset();

3699
z3.log Normal file
View file

File diff suppressed because it is too large Load diff