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

Giving up is still no conflict

Browse source
This commit is contained in:
CEisenhofer 2026-06-11 16:27:59 +02:00
parent b9d5f273ee
commit f126b60369
2 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_nseq.cpp
View file

@ -613,8 +613,15 @@ namespace smt {
split_set pairs;
auto [head, tail] = seq::split_membership(mem.m_str, mem.m_regex, m_sg, threshold, pairs);
if (!head) {
// gave up
SASSERT(!tail);
return;
}
SASSERT(tail);
if (pairs.empty()) {
// no viable splits
literal_vector lits;
lits.push_back(mem.lit);
set_conflict(lits);

2
src/smt/theory_nseq.h
View file

@ -136,7 +136,7 @@ namespace smt {
// private helpers
void populate_nielsen_graph();
void explain_nielsen_conflict();
void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits);
void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits) const;
void set_conflict(literal_vector const& lits) {
const enode_pair_vector eqs;
set_conflict(eqs, lits);