Skip to content

Commit b395875

Browse files
committed
fixing wrc20 test
1 parent 2a67a33 commit b395875

File tree

3 files changed

+2728
-14
lines changed

3 files changed

+2728
-14
lines changed

test/regression-wasm-semantics-5372938/generate.sh

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,5 @@ do
3434
done
3535

3636
kollect "test-wrc20" \
37-
./kwasm prove --backend haskell \
38-
tests/proofs/wrc20-spec.k \
39-
WRC20-LEMMAS
37+
./kwasm prove --backend haskell tests/proofs/wrc20-spec.k WRC20-LEMMAS --format-failures \
38+
--concrete-rules WASM-DATA.wrap-Positive,WASM-DATA.setRange-Positive,WASM-DATA.getRange-Positive,WASM-DATA.get-Existing,WASM-DATA.set-Extend

0 commit comments

Comments
 (0)