From ebd35bc5a3ff5f96a754e1c117e7120abe42e2c0 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 26 Mar 2026 17:32:41 +0100 Subject: [PATCH] Avoid doing extensions steps twice, as the bounds are recognized too late --- src/smt/seq/seq_nielsen.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index c7637f4c4..0d803a563 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1430,6 +1430,9 @@ namespace seq { return search_result::unknown; } 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) const simplify_result sr = node->simplify_and_init(cur_path);