mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 14:56:11 +00:00
Code Activity

Misclassified giving-up on decomposition as conflict

Browse source
This commit is contained in:
CEisenhofer 2026-06-09 16:22:41 +02:00
parent 8229bcc5fc
commit 2e4c165a16
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3713,7 +3713,11 @@ namespace seq {
return false; return false;
for (unsigned i = 1; i < n && !current.empty(); ++i) { for (unsigned i = 1; i < n && !current.empty(); ++i) {
sigma_pairs arg_i; sigma_pairs arg_i;
compute_sigma(m, seq, rw, r->arg(i), arg_i, threshold); // A give-up on any conjunct must propagate as a give-up: silently
// treating arg_i as the empty split-set would collapse the whole
// intersection to ∅ and be misreported as an (unsound) conflict.
if (!compute_sigma(m, seq, rw, r->arg(i), arg_i, threshold))
return false;
sigma_pairs tmp; sigma_pairs tmp;
if (!intersect_sigma_pairs(m, seq, current, arg_i, tmp, threshold)) if (!intersect_sigma_pairs(m, seq, current, arg_i, tmp, threshold))
return false; return false;