mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
added assertion
This commit is contained in:
parent
f128c76f23
commit
dbf9609b4c
|
@ -167,6 +167,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
|
|||
|
||||
void pop(unsigned num_scopes) {
|
||||
if (num_scopes > 0) {
|
||||
SASSERT(num_scopes <= m_keyval_lim.size());
|
||||
unsigned new_sz = m_keyval_lim.size() - num_scopes;
|
||||
unsigned lim = m_keyval_lim[new_sz];
|
||||
for (unsigned i = m_keys.size(); i > lim; ) {
|
||||
|
|
Loading…
Reference in a new issue