ci: use jsi for snekmate test (#415)

a16z · Nov 16, 2024 · d4cac2e · d4cac2e
1 parent ce13a9f
commit d4cac2e
Showing 1 changed file with 11 additions and 11 deletions.
diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml
@@ -22,52 +22,52 @@ jobs:
         project:
           - repo: "morpho-org/morpho-data-structures"
             dir: "morpho-data-structures"
-            cmd: "--function testProve --loop 4"
+            cmd: "--function testProve --loop 4 --solver-command yices-smt2 --solver-threads 3"
             branch: ""
             profile: ""
           - repo: "morpho-org/morpho-blue"
             dir: "morpho-blue"
-            cmd: ""
+            cmd: "--solver-command yices-smt2 --solver-threads 3"
             branch: ""
             profile: "test"
           - repo: "a16z/cicada"
             dir: "cicada"
-            cmd: "--contract LibUint1024Test --function testProve --loop 256"
+            cmd: "--contract LibUint1024Test --function testProve --loop 256 --solver-command yices-smt2 --solver-threads 3"
             branch: ""
             profile: ""
           - repo: "a16z/cicada"
             dir: "cicada"
-            cmd: "--contract LibPrimeTest --function testProve --loop 256"
+            cmd: "--contract LibPrimeTest --function testProve --loop 256 --solver-command yices-smt2 --solver-threads 3"
             branch: ""
             profile: ""
           - repo: "farcasterxyz/contracts"
             dir: "farcaster-contracts"
-            cmd: ""
+            cmd: "--solver-command yices-smt2 --solver-threads 3"
             branch: ""
             profile: ""
           - repo: "zobront/halmos-solady"
             dir: "halmos-solady"
-            cmd: "--function testCheck"
+            cmd: "--function testCheck --solver-command yices-smt2 --solver-threads 3"
             branch: ""
             profile: ""
           - repo: "pcaversaccio/snekmate"
             dir: "snekmate"
-            cmd: "--config test/halmos.toml --contract ERC20TestHalmos"
+            cmd: "--config test/halmos.toml --contract ERC20TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
             branch: ""
             profile: "halmos"
           - repo: "pcaversaccio/snekmate"
             dir: "snekmate"
-            cmd: "--config test/halmos.toml --contract ERC721TestHalmos"
+            cmd: "--config test/halmos.toml --contract ERC721TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
             branch: ""
             profile: "halmos"
           - repo: "pcaversaccio/snekmate"
             dir: "snekmate"
-            cmd: "--config test/halmos.toml --contract ERC1155TestHalmos"
+            cmd: "--config test/halmos.toml --contract ERC1155TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
             branch: ""
             profile: "halmos"
           - repo: "pcaversaccio/snekmate"
             dir: "snekmate"
-            cmd: "--config test/halmos.toml --contract MathTestHalmos"
+            cmd: "--config test/halmos.toml --contract MathTestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
             branch: ""
             profile: "halmos"
 
@@ -110,7 +110,7 @@ jobs:
         run: docker run halmos-image halmos --version
 
       - name: Test external repo
-        run: docker run -e FOUNDRY_PROFILE -v .:/workspace halmos-image halmos ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 3 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}
+        run: docker run -e FOUNDRY_PROFILE -v .:/workspace halmos-image halmos ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}
         working-directory: ${{ matrix.project.dir }}
         env:
           FOUNDRY_PROFILE: ${{ matrix.project.profile }}