mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 19:21:22 +00:00
Code Activity

propagate before push

Browse source
This commit is contained in:
Jakob Rath 2023-03-23 09:35:10 +01:00
parent 51025a75b4
commit d2397deb8d
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/solver.cpp
View file

@ -1426,6 +1426,7 @@ namespace polysat {
void solver::push() { void solver::push() {
LOG_H3("Push user scope"); LOG_H3("Push user scope");
propagate();
push_level(); push_level();
m_base_levels.push_back(m_level); m_base_levels.push_back(m_level);
m_base_index.push_back(m_search.size()); m_base_index.push_back(m_search.size());