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

Disequalities prevent a fast-check

Browse source
This commit is contained in:
CEisenhofer 2026-05-27 17:59:14 +02:00
parent dc7c94a3ac
commit c640bf2a2b
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

@ -1454,9 +1454,10 @@ namespace smt {
// Collect mem items from the propagation queue into a local pointer array // Collect mem items from the propagation queue into a local pointer array
// so that indices into the array remain stable during this function. // so that indices into the array remain stable during this function.
ptr_vector<tracked_str_mem const> mems; ptr_vector<tracked_str_mem const> mems;
for (auto const& item : m_prop_queue) for (auto const& item : m_prop_queue) {
if (std::holds_alternative<mem_item>(item)) if (std::holds_alternative<mem_item>(item))
mems.push_back(&std::get<mem_item>(item)); mems.push_back(&std::get<mem_item>(item));
}
if (mems.empty()) if (mems.empty())
return l_undef; return l_undef;
@ -1481,7 +1482,7 @@ namespace smt {
return l_undef; return l_undef;
// Check if there are any eq items in the queue (needed for SAT condition below). // Check if there are any eq items in the queue (needed for SAT condition below).
bool has_eqs = any_of(m_prop_queue, [](auto p) { return std::holds_alternative<eq_item>(p); }); bool has_eqs = any_of(m_prop_queue, [](auto p) { return std::holds_alternative<eq_item>(p) || std::holds_alternative<deq_item>(p); });
bool any_undef = false; bool any_undef = false;