From beda426d7cde3729d7e64fc36a79986e550b8886 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 1 Apr 2026 17:21:11 +0200 Subject: [PATCH] Integer conflicts are proper conflicts --- src/smt/seq/seq_nielsen.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 6d923cf14..acf774c48 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1432,6 +1432,7 @@ namespace seq { if (!cur_path.empty() && !check_int_feasibility()) { dep_tracker dep = get_subsolver_dependency(node); node->set_conflict(backtrack_reason::arithmetic, dep); + node->set_general_conflict(true); ++m_stats.m_num_arith_infeasible; return search_result::unsat; }