mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

Mark quantifier instances that lead to conflicts as relevant

Browse source
This commit is contained in:
Can Cebeci 2026-07-07 11:07:09 -07:00
parent ff7e22c055
commit c03cda14f1
1 changed files with 11 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/smt_context.h
View file

@ -1733,8 +1733,18 @@ namespace smt {
void internalize_instance(expr * body, proof * pr, unsigned generation) {
internalize_assertion(body, pr, generation);
if (relevancy())
if (relevancy()) {
if (inconsistent()) {
app * a = to_app(body);
SASSERT(a->get_decl_kind() == OP_OR);
SASSERT(to_app(a->get_arg(0))->get_decl_kind() == OP_NOT);
SASSERT(is_quantifier(to_app(a->get_arg(0))->get_arg(0)));
for (unsigned i = 1; i < a->get_num_args(); ++i) {
mark_as_relevant(a->get_arg(i));
}
}
m_case_split_queue->internalize_instance_eh(body, generation);
}
}
unsigned get_unsat_core_size() const {