mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 06:07:46 +00:00
Code Activity

Integer conflicts are proper conflicts

Browse source
This commit is contained in:
CEisenhofer 2026-04-01 17:21:11 +02:00
parent 36b01a51f1
commit beda426d7c
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1432,6 +1432,7 @@ namespace seq {
if (!cur_path.empty() && !check_int_feasibility()) { if (!cur_path.empty() && !check_int_feasibility()) {
dep_tracker dep = get_subsolver_dependency(node); dep_tracker dep = get_subsolver_dependency(node);
node->set_conflict(backtrack_reason::arithmetic, dep); node->set_conflict(backtrack_reason::arithmetic, dep);
node->set_general_conflict(true);
++m_stats.m_num_arith_infeasible; ++m_stats.m_num_arith_infeasible;
return search_result::unsat; return search_result::unsat;
} }