mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-06 04:36:08 +00:00
Code Activity

Fix problem with divisibility predicate

Browse source
This commit is contained in:
CEisenhofer 2026-04-02 16:25:49 +02:00
parent 5ec28d3bc8
commit a8db876765
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_nseq.cpp
View file

@ -592,7 +592,8 @@ namespace smt {
// all regex constraints satisfiable, no word eqs → SAT
IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck SAT\n";);
m_nielsen.set_sat_node(m_nielsen.root());
if (!check_length_coherence()) return FC_CONTINUE;
if (!check_length_coherence())
return FC_CONTINUE;
TRACE(seq, display(tout << "pre-check done\n"));
return FC_DONE;
default:
@ -1240,7 +1241,7 @@ namespace smt {
expr_ref len_minus_l(m_autil.mk_sub(len_expr, l_expr), m);
expr_ref not_divides(m.mk_not(m_autil.mk_divides(g_expr, len_minus_l)), m);
prop_expr = m.mk_or(len_lt_l, not_divides);
std::cout << "Propagating " << mk_pp(prop_expr, m) << " for length " << l << " with gradient " << g << std::endl;
m_th_rewriter(prop_expr); // the divisibility predicate needs to be rewritten as it won't happen automatically
m_gradient_cache[s] = 1; // Reset gradient cache
}