Re-enable test store.wat

[krtab]

Test was to slow because once the out of bounds cases have been ruled out, all "in bounds" cases still have to concretize a value for the symbol and perform the store, leading to approx. <page_size> calls to Z3.

By reducing the possible values of idx, we ensure that the test runs fast.

Closes #177

[zapashcanon]

I understand that this now passes the test but I'm a little bit worried: are we going to have to insert such assume in any code we want to test ? I'm wondering if there is not a way to solve this in Owi directly... it probably means waiting for the new memory model ?

[krtab]

I don't think there is a one size fits all solution.
We could have a lazier memory model, or one more symbolic. For real life applications, we can accept that exploration will anyway never be total and rely on a future exploration heuristic to ensure that all interesting cases are explored first. We can then time out after a while, and assume that the remaining cases would only lead to uninteresting behaviors (or even prove it and discard them entirely?).

[zapashcanon]

Thanks!