diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index 657b2a85..f9f41449 100644 --- 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 }}