mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-27 10:58:48 +00:00
Code Activity

Copy elements from propagation queue before propagating them. The memory might get invalidated inbetween

Browse source
This commit is contained in:
CEisenhofer 2026-06-26 11:08:54 +02:00
parent d2db79e1a7
commit ff7cbe9406
3 changed files with 18 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
scripts/compare_seq_solvers.py
View file

@ -38,7 +38,7 @@ COMMON_ARGS = ["model_validate=true"]
SOLVERS = {
"nseq_md": ["smt.string_solver=nseq", "smt.nseq.parikh=false",
"smt.nseq.regex_factorization_threshold=100", "smt.nseq.regex_factorization_eager=true"],
"nseq_pa": ["smt.string_solver=nseq", "smt.nseq.parikh=true",
"nseq_pa": ["smt.string_solver=nseq", "smt.nseq.parikh=false",
"smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false"],
"seq": ["smt.string_solver=seq"],
}

23
src/smt/theory_nseq.cpp
View file

@ -463,14 +463,23 @@ namespace smt {
ctx.push_trail(value_trail(m_prop_qhead));
while (m_prop_qhead < m_prop_queue.size() && !ctx.inconsistent()) {
auto const& item = m_prop_queue[m_prop_qhead++];
if (std::holds_alternative<eq_item>(item))
propagate_eq(std::get<eq_item>(item));
else if (std::holds_alternative<deq_item>(item))
propagate_deq(std::get<deq_item>(item));
else if (std::holds_alternative<mem_item>(item))
propagate_pos_mem(std::get<mem_item>(item));
else if (std::holds_alternative<axiom_item>(item))
// don't pass arguments via reference. They might tigger internalization
// and so the references from the propagation queue might change
if (std::holds_alternative<eq_item>(item)) {
const auto eq = std::get<eq_item>(item);
propagate_eq(eq);
}
else if (std::holds_alternative<deq_item>(item)) {
const auto deq = std::get<deq_item>(item);
propagate_deq(deq);
}
else if (std::holds_alternative<mem_item>(item)) {
const auto mem = std::get<mem_item>(item);
propagate_pos_mem(mem);
}
else if (std::holds_alternative<axiom_item>(item)) {
dequeue_axiom(std::get<axiom_item>(item).e);
}
else {
UNREACHABLE();
}

1
src/smt/theory_nseq.h
View file

@ -153,6 +153,7 @@ namespace smt {
void propagate_eq(tracked_str_eq const& eq) const;
void propagate_deq(tracked_str_deq const& deq) const;
void propagate_pos_mem(tracked_str_mem const& mem);
void enqueue_axiom(expr* e);
void dequeue_axiom(expr* e);
void ensure_length_var(expr* e) const;