| 559 | } |
| 560 | |
| 561 | bool Memory::isInitialMemoryOrLoad(const expr &e, bool match_any_init) { |
| 562 | expr arr, idx; |
| 563 | if (e.isLoad(arr, idx)) |
| 564 | return isInitialMemoryOrLoad(arr, match_any_init); |
| 565 | |
| 566 | expr val; |
| 567 | unsigned hi, lo; |
| 568 | if (e.isExtract(val, hi, lo)) |
| 569 | return isInitialMemoryOrLoad(val, match_any_init); |
| 570 | |
| 571 | return isInitialMemBlock(e, match_any_init) != 0; |
| 572 | } |
| 573 | } |
| 574 | |
| 575 | static void pad(StateValue &v, unsigned amount, State &s) { |