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

Update smt_context.h

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-07 11:46:56 -07:00 • committed by GitHub
parent c03cda14f1
commit 828e7a4ed6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/smt_context.h
View file

@ -1734,14 +1734,12 @@ namespace smt {
void internalize_instance(expr * body, proof * pr, unsigned generation) {
internalize_assertion(body, pr, generation);
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));
}
// if the instantiation creates a conflict, we backtrack immediately.
// to retain the conflict clause being relevant we mark it here.
// if the instantiation does not create a conflict, default relevancy propagation applies.
if (inconsistent() && is_app(body)) {
for (auto arg : *to_app(body))
mark_as_relevant(arg);
}
m_case_split_queue->internalize_instance_eh(body, generation);
}