From 3397b7c9a93179c2576dc168d4cefdfcf27dac73 Mon Sep 17 00:00:00 2001 From: Malcolm Langfield <35980963+langfield@users.noreply.github.com> Date: Tue, 28 Mar 2023 07:58:54 -0400 Subject: [PATCH] Add mathsat installation to Github actions workflow * Use `ssh-agent` to clone with specific private key * Set `0o400` permissions on private key file * Add `mathsat` to list of solvers used in tests --- .github/workflows/main.yml | 5 +++++ tests/resources/bats-template | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index c6a8cd06..486a9c14 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -68,8 +68,13 @@ jobs: - name: Install SMT solvers run: | + echo "${{ secrets.MATHSAT_INSTALL_DEPLOY_KEY }}" >> mathsat_id_ed25519 + chmod 400 mathsat_id_ed25519 + ssh-agent bash -c 'ssh-add mathsat_id_ed25519; git clone git@github.com:NethermindEth/mathsat-install.git' + cp mathsat-install/install-mathsat.sh ./scripts/ci/install-mathsat.sh sh ./scripts/ci/install-z3-linux-amd64.sh sh ./scripts/ci/install-cvc5-linux.sh + sh ./scripts/ci/install-mathsat.sh - uses: actions/setup-python@v4 with: diff --git a/tests/resources/bats-template b/tests/resources/bats-template index e4da0475..db4506cc 100644 --- a/tests/resources/bats-template +++ b/tests/resources/bats-template @@ -26,7 +26,7 @@ test_case() { temp_file="${base}.temp" horus-compile "$test_file" --output "$compiled_file" --spec_output "$spec_file" - stack run horus-check "$compiled_file" "$spec_file" -- -s cvc5 -s z3 -t 100000 &> "$temp_file" || true + stack run horus-check "$compiled_file" "$spec_file" -- -s cvc5 -s mathsat -s z3 -t 100000 &> "$temp_file" || true compare "${gold_file}" "${temp_file}" rm "$compiled_file" rm "$spec_file"