mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

for #2039

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-12-18 11:27:04 -08:00
parent b6bf299b8b
commit 35e8decdb1
4 changed files with 6 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/asserted_formulas.cpp
View file

@ -449,7 +449,7 @@ void asserted_formulas::propagate_values() {
m_expr2depth.reset();
m_scoped_substitution.push();
unsigned prop = num_prop;
TRACE("propagate_values", tout << "before:\n"; display(tout););
TRACE("propagate_values", display(tout << "before:\n"););
unsigned i = m_qhead;
unsigned sz = m_formulas.size();
for (; i < sz; i++) {
@ -482,15 +482,13 @@ unsigned asserted_formulas::propagate_values(unsigned i) {
expr_ref new_n(m);
proof_ref new_pr(m);
m_rewriter(n, new_n, new_pr);
TRACE("propagate_values", tout << n << "\n" << new_n << "\n";);
if (m.proofs_enabled()) {
proof * pr = m_formulas[i].get_proof();
new_pr = m.mk_modus_ponens(pr, new_pr);
}
justified_expr j(m, new_n, new_pr);
m_formulas[i] = j;
if (m_formulas[i].get_fml() != new_n) {
std::cout << "NOT updated\n";
}
if (m.is_false(j.get_fml())) {
m_inconsistent = true;
}