mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Reverted reusing can_propagate (#5966)

Browse source 
* Fixed registering expressions in push/pop

* Reused existing function

* Reverted reusing can_propagate
This commit is contained in:
Clemens Eisenhofer 2022-04-12 12:29:53 +02:00 committed by GitHub
parent ac55e29a56
commit b264e6c290
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_user_propagator.cpp
View file

@ -133,7 +133,7 @@ final_check_status theory_user_propagator::final_check_eh() {
}
propagate();
// check if it became inconsistent or something new was propagated/registered
bool done = !can_propagate() && !ctx.inconsistent();
bool done = (sz1 == m_prop.size()) && (sz2 == m_expr2var.size()) && !ctx.inconsistent();
return done ? FC_DONE : FC_CONTINUE;
}