Re-enable test store.wat

test/sym/memory.t

@@ -8,14 +8,12 @@ memory stuff:
       (symbol_0 (i32 1)))
   Reached problem!
   [13]
-# Deactivated because it is currently an enumeration of all i32s with the forced concretization
-#  $ dune exec owi -- sym store.wat
-#  Trap: out of bounds memory access
-#  Model:
-#    (model
-#      (symbol_0 (i32 -11))
-#      (symbol_1 (i32 0)))
-#  Reached problem!
-#  [1]
+  $ dune exec owi -- sym store.wat
+  Trap: out of bounds memory access
+  Model:
+    (model
+      (symbol_0 (i32 2146549760)))
+  Reached problem!
+  [13]
   $ dune exec owi -- sym memory2.wat
   All OK

test/sym/store.wat

@@ -1,5 +1,6 @@
 (module
   (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+  (import "symbolic" "assume" (func $owi_assume (param i32)))
 
   (memory $m 1)
 
@@ -8,9 +9,15 @@
 
     (local $idx i32)
 
-    (local.tee $idx (call $i32_symbol))
-    call $i32_symbol
-    i32.store
+    (local.set  $idx (call $i32_symbol))
+
+    ;; Hackish way to reduce the size of the search space. Otherwise, all possible
+    ;; values of idx between 0 and <page_size> get checked.
+    (call $owi_assume
+      (i32.eqz (i32.rem_s (local.get $idx) (i32.const 4096)))
+    )
+
+    (i32.store (local.get $idx) (i32.const 42))
   )
 
   (start $start)