mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-25 13:23:32 +00:00
Code Activity

Avoid doing extensions steps twice, as the bounds are recognized too late

Browse source
This commit is contained in:
CEisenhofer 2026-03-26 17:32:41 +01:00
parent dcc85cf9ef
commit ebd35bc5a3
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1430,6 +1430,9 @@ namespace seq {
return search_result::unknown; return search_result::unknown;
} }
node->set_eval_idx(m_run_idx); node->set_eval_idx(m_run_idx);
// we might need to tell the SAT solver about the new integer inequalities
// that might have been added by an extension step
assert_node_new_int_constraints(node);
// simplify constraints (idempotent after first call) // simplify constraints (idempotent after first call)
const simplify_result sr = node->simplify_and_init(cur_path); const simplify_result sr = node->simplify_and_init(cur_path);