Update all regression-evm tests

runtimeverification · Oct 25, 2023 · d960a77 · d960a77
1 parent 707f73c
commit d960a77
Show file tree

Hide file tree

Showing 21 changed files with 151,375 additions and 80,125 deletions.
diff --git a/test/regression-evm/test-dsvalue-peek-pass-rough-definition.kore b/test/regression-evm/test-dsvalue-peek-pass-rough-definition.kore
diff --git a/test/regression-evm/test-dsvalue-peek-pass-rough-spec.kore b/test/regression-evm/test-dsvalue-peek-pass-rough-spec.kore
diff --git a/test/regression-evm/test-dsvalue-peek-pass-rough.sh b/test/regression-evm/test-dsvalue-peek-pass-rough.sh
@@ -5,13 +5,18 @@ exec kore-exec \
     --module VERIFICATION \
     --strategy all \
     --max-counterexamples 1 \
-    --smt-timeout 99 \
-    --smt-retry-limit 1 \
+    --smt-timeout 125 \
+    --smt-retry-limit 3 \
     --smt-reset-interval 100 \
     --smt z3 \
+    --log \
+    /home/sguest/work/haskell-backend/evm-semantics/tests/specs/mcd/dsvalue-peek-pass-rough-spec.debug-log \
+    --log-format=oneline \
     --log-level \
     warning \
     --enable-log-timestamps \
+    --log-entries \
+    DebugTransition \
     --prove test-dsvalue-peek-pass-rough-spec.kore \
     --spec-module DSVALUE-PEEK-PASS-ROUGH-SPEC \
     --graph-search breadth-first \

diff --git a/test/regression-evm/test-flipper-addu48u48-fail-rough-definition.kore b/test/regression-evm/test-flipper-addu48u48-fail-rough-definition.kore
diff --git a/test/regression-evm/test-flipper-addu48u48-fail-rough-spec.kore b/test/regression-evm/test-flipper-addu48u48-fail-rough-spec.kore
diff --git a/test/regression-evm/test-flipper-addu48u48-fail-rough.sh b/test/regression-evm/test-flipper-addu48u48-fail-rough.sh
@@ -5,13 +5,18 @@ exec kore-exec \
     --module VERIFICATION \
     --strategy all \
     --max-counterexamples 1 \
-    --smt-timeout 99 \
-    --smt-retry-limit 1 \
+    --smt-timeout 125 \
+    --smt-retry-limit 3 \
     --smt-reset-interval 100 \
     --smt z3 \
+    --log \
+    /home/sguest/work/haskell-backend/evm-semantics/tests/specs/mcd/flipper-addu48u48-fail-rough-spec.debug-log \
+    --log-format=oneline \
     --log-level \
     warning \
     --enable-log-timestamps \
+    --log-entries \
+    DebugTransition \
     --prove test-flipper-addu48u48-fail-rough-spec.kore \
     --spec-module FLIPPER-ADDU48U48-FAIL-ROUGH-SPEC \
     --graph-search breadth-first \