mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Bugfix relevancy propagation + UP (old core) (#6678)

Browse source 
* Some UP bugfixes in the new core

* Bugfix relevancy propagation + UP (old core)

* Revert smt_context.cpp
This commit is contained in:
Clemens Eisenhofer 2023-04-10 21:57:59 +02:00 committed by GitHub
parent 4a142b0f81
commit 98d3fabc24
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_user_propagator.cpp
View file

@ -92,6 +92,9 @@ void theory_user_propagator::propagate_cb(
expr_ref _conseq(conseq, m);
ctx.get_rewriter()(conseq, _conseq);
if (!ctx.get_manager().is_true(_conseq) && !ctx.get_manager().is_false(_conseq))
ctx.mark_as_relevant((expr*)_conseq);
if (ctx.lit_internalized(_conseq) && ctx.get_assignment(ctx.get_literal(_conseq)) == l_true)
return;
m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, _conseq));