mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-30 07:53:15 +00:00
Code Activity

Some more commenting

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-12-25 12:51:13 +01:00
parent 74ec28201e
commit 52eefb6e85
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/fixed_bits.cpp
View file

@ -607,10 +607,13 @@ namespace polysat {
} }
void fixed_bits::push() { void fixed_bits::push() {
#if 0
m_trail_size.push_back(m_trail.size()); m_trail_size.push_back(m_trail.size());
#endif
} }
void fixed_bits::pop(unsigned pop_cnt) { void fixed_bits::pop(unsigned pop_cnt) {
#if 0
SASSERT(!m_consistent); // Why do we backtrack if this is true? We might remove this for (random) restarts SASSERT(!m_consistent); // Why do we backtrack if this is true? We might remove this for (random) restarts
SASSERT(pop_cnt > 0); SASSERT(pop_cnt > 0);
@ -642,6 +645,7 @@ namespace polysat {
m_trail.resize(prev_cnt); m_trail.resize(prev_cnt);
else else
m_trail.resize(last_to_keep); m_trail.resize(last_to_keep);
#endif
} }
#define COUNT(DOWN, TO_COUNT) \ #define COUNT(DOWN, TO_COUNT) \