mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
remove dependency on pragma
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
dead0c9de2
commit
111d27cbee
|
@ -310,17 +310,15 @@ public:
|
||||||
}
|
}
|
||||||
|
|
||||||
void check_size(cell* c) const {
|
void check_size(cell* c) const {
|
||||||
[[maybe_unused]] unsigned r;
|
|
||||||
while (c) {
|
while (c) {
|
||||||
switch (c->kind()) {
|
switch (c->kind()) {
|
||||||
case SET:
|
case SET:
|
||||||
break;
|
break;
|
||||||
case PUSH_BACK:
|
case PUSH_BACK:
|
||||||
r = size(c->next());
|
// ? SASSERT(c->idx() == size(c->next()));
|
||||||
break;
|
break;
|
||||||
case POP_BACK:
|
case POP_BACK:
|
||||||
r = size(c->next());
|
SASSERT(c->idx() == size(c->next()));
|
||||||
SASSERT(c->idx() == r);
|
|
||||||
break;
|
break;
|
||||||
case ROOT:
|
case ROOT:
|
||||||
return;
|
return;
|
||||||
|
|
Loading…
Reference in a new issue