diff --git a/test/sym/memory.t b/test/sym/memory.t index 35a79d717..2971f4fa9 100644 --- a/test/sym/memory.t +++ b/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 diff --git a/test/sym/store.wat b/test/sym/store.wat index d1aa26bbe..cfc82723e 100644 --- a/test/sym/store.wat +++ b/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 gets 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)