mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-03 05:46:08 +00:00
Code Activity

Bug in model extraction

Browse source 
Added debug check
This commit is contained in:
CEisenhofer 2026-04-08 16:37:21 +02:00
parent 26d36ba6ee
commit 74cf21b852
2 changed files with 24 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/seq_model.cpp
View file

@ -171,6 +171,12 @@ namespace smt {
if (n->is_char() || n->is_unit()) { if (n->is_char() || n->is_unit()) {
expr* e = n->get_expr(); expr* e = n->get_expr();
expr_ref val(m);
if (e && m_int_model) {
m_int_model->eval_expr(e, val, true);
if (val)
return val;
}
return e ? expr_ref(e, m) : expr_ref(m); return e ? expr_ref(e, m) : expr_ref(m);
} }

19
src/smt/theory_nseq.cpp
View file

@ -752,7 +752,7 @@ namespace smt {
else else
kernel.assert_expr(ctx.literal2expr(std::get<sat::literal>(d))); kernel.assert_expr(ctx.literal2expr(std::get<sat::literal>(d)));
} }
const auto res = kernel.check(); auto res = kernel.check();
if (res == l_true) { if (res == l_true) {
std::cout << "Insufficient justification:\n"; std::cout << "Insufficient justification:\n";
for (auto& lit : lits) { for (auto& lit : lits) {
@ -763,6 +763,23 @@ namespace smt {
} }
auto dot = m_nielsen.to_dot(); auto dot = m_nielsen.to_dot();
std::cout << std::endl; std::cout << std::endl;
kernel.reset();
for (const seq::constraint& c : m_nielsen.root()->constraints()) {
kernel.assert_expr(c.fml);
}
for (const seq::str_eq& c : m_nielsen.root()->str_eqs()) {
kernel.assert_expr(m.mk_eq(c.m_lhs->get_expr(), c.m_rhs->get_expr()));
}
for (const seq::str_mem& c : m_nielsen.root()->str_mems()) {
kernel.assert_expr(m_seq.re.mk_in_re(c.m_str->get_expr(), c.m_regex->get_expr()));
}
res = kernel.check();
if (res == l_true)
// the algorithm is unsound
std::cout << "Original input is SAT" << std::endl;
else if (res == l_false)
// the justification is too narrow
std::cout << "Original input is UNSAT" << std::endl;
} }
VERIFY(res != l_true); VERIFY(res != l_true);
} }