| 2083 | } |
| 2084 | |
| 2085 | expr expr::store(const expr &idx, const expr &val) const { |
| 2086 | C(idx, val); |
| 2087 | expr array, str_idx, str_val; |
| 2088 | if (isStore(array, str_idx, str_val)) { |
| 2089 | if ((idx == str_idx).isTrue()) |
| 2090 | return array.store(idx, val); |
| 2091 | |
| 2092 | } else if (isConstArray(str_val)) { |
| 2093 | if (str_val.eq(val)) |
| 2094 | return *this; |
| 2095 | } |
| 2096 | return Z3_mk_store(ctx(), ast(), idx(), val()); |
| 2097 | } |
| 2098 | |
| 2099 | expr expr::load(const expr &idx, uint64_t max_idx) const { |
| 2100 | C(idx); |