mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-21 11:23:30 +00:00
Code Activity

recompiled

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-20 16:32:44 -07:00
parent 488c02711d
commit ccdfdbb176
17 changed files with 998 additions and 604 deletions
Download patch file Download diff file Expand all files Collapse all files

91
.github/workflows/qf-s-benchmark.lock.yml generated vendored
View file

@ -13,7 +13,7 @@
# \ /\ / (_) | | | | ( | | | | (_) \ V V /\__ \
# \/ \/ \___/|_| |_|\_\|_| |_|\___/ \_/\_/ |___/
#
# This file was automatically generated by gh-aw (v0.53.4). DO NOT EDIT.
# This file was automatically generated by gh-aw (v0.57.2). DO NOT EDIT.
#
# To update this file, edit the corresponding .md file and run:
# gh aw compile
@ -23,9 +23,9 @@
#
# Run Z3 string solver benchmarks (seq vs nseq) on QF_S test suite from the c3 branch and post results as a GitHub discussion
#
# gh-aw-metadata: {"schema_version":"v1","frontmatter_hash":"7ab3bd2bbf01cbc03e57737e0508a5e8981db23cc44b9442ce396f40f26516e0","compiler_version":"v0.53.4"}
# gh-aw-metadata: {"schema_version":"v2","frontmatter_hash":"6544f1125ef010e1b4d85a5d0e4e43ceb5edf7d708c4135b62116975eb8935bd","compiler_version":"v0.57.2","strict":true}
name: "Qf S Benchmark"
name: "ZIPT String Solver Benchmark"
"on":
schedule:
- cron: "0 0,12 * * *"
@ -36,7 +36,7 @@ permissions: {}
concurrency:
group: "gh-aw-${{ github.workflow }}"
run-name: "Qf S Benchmark"
run-name: "ZIPT String Solver Benchmark"
jobs:
activation:
@ -50,7 +50,7 @@ jobs:
secret_verification_result: ${{ steps.validate-secret.outputs.verification_result }}
steps:
- name: Setup Scripts
uses: github/gh-aw/actions/setup@7d1a2798f21c06247ce115b7c7b8ddd70c8d0dc3 # v0.59.0
uses: github/gh-aw/actions/setup@32b3a711a9ee97d38e3989c90af0385aff0066a7 # v0.57.2
with:
destination: /opt/gh-aw/actions
- name: Generate agentic run info
@ -60,9 +60,9 @@ jobs:
GH_AW_INFO_ENGINE_NAME: "GitHub Copilot CLI"
GH_AW_INFO_MODEL: ${{ vars.GH_AW_MODEL_AGENT_COPILOT || '' }}
GH_AW_INFO_VERSION: ""
GH_AW_INFO_AGENT_VERSION: "0.0.421"
GH_AW_INFO_CLI_VERSION: "v0.53.4"
GH_AW_INFO_WORKFLOW_NAME: "Qf S Benchmark"
GH_AW_INFO_AGENT_VERSION: "latest"
GH_AW_INFO_CLI_VERSION: "v0.57.2"
GH_AW_INFO_WORKFLOW_NAME: "ZIPT String Solver Benchmark"
GH_AW_INFO_EXPERIMENTAL: "false"
GH_AW_INFO_SUPPORTS_TOOLS_ALLOWLIST: "true"
GH_AW_INFO_STAGED: "false"
@ -71,6 +71,7 @@ jobs:
GH_AW_INFO_AWF_VERSION: "v0.23.0"
GH_AW_INFO_AWMG_VERSION: ""
GH_AW_INFO_FIREWALL_TYPE: "squid"
GH_AW_COMPILED_STRICT: "true"
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
with:
script: |
@ -84,12 +85,12 @@ jobs:
- name: Checkout .github and .agents folders
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
with:
persist-credentials: false
sparse-checkout: |
.github
.agents
sparse-checkout-cone-mode: true
fetch-depth: 1
persist-credentials: false
- name: Check workflow file timestamps
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
env:
@ -166,6 +167,8 @@ jobs:
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
env:
GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
GH_AW_GITHUB_REPOSITORY: ${{ github.repository }}
GH_AW_GITHUB_WORKSPACE: ${{ github.workspace }}
with:
script: |
const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
@ -215,7 +218,7 @@ jobs:
run: bash /opt/gh-aw/actions/print_prompt_summary.sh
- name: Upload activation artifact
if: success()
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7
with:
name: activation
path: |
@ -250,13 +253,13 @@ jobs:
output_types: ${{ steps.collect_output.outputs.output_types }}
steps:
- name: Setup Scripts
uses: github/gh-aw/actions/setup@7d1a2798f21c06247ce115b7c7b8ddd70c8d0dc3 # v0.59.0
uses: github/gh-aw/actions/setup@32b3a711a9ee97d38e3989c90af0385aff0066a7 # v0.57.2
with:
destination: /opt/gh-aw/actions
- name: Create gh-aw temp directory
run: bash /opt/gh-aw/actions/create_gh_aw_tmp_dir.sh
- name: Checkout c3 branch
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
with:
fetch-depth: 1
persist-credentials: false
@ -289,7 +292,7 @@ jobs:
const { main } = require('/opt/gh-aw/actions/checkout_pr_branch.cjs');
await main();
- name: Install GitHub Copilot CLI
run: /opt/gh-aw/actions/install_copilot_cli.sh 0.0.421
run: /opt/gh-aw/actions/install_copilot_cli.sh latest
- name: Install awf binary
run: bash /opt/gh-aw/actions/install_awf_binary.sh v0.23.0
- name: Determine automatic lockdown mode for GitHub MCP Server
@ -303,7 +306,7 @@ jobs:
const determineAutomaticLockdown = require('/opt/gh-aw/actions/determine_automatic_lockdown.cjs');
await determineAutomaticLockdown(github, context, core);
- name: Download container images
run: bash /opt/gh-aw/actions/download_docker_images.sh ghcr.io/github/gh-aw-firewall/agent:0.23.0 ghcr.io/github/gh-aw-firewall/api-proxy:0.23.0 ghcr.io/github/gh-aw-firewall/squid:0.23.0 ghcr.io/github/gh-aw-mcpg:v0.1.8 ghcr.io/github/github-mcp-server:v0.31.0 node:lts-alpine
run: bash /opt/gh-aw/actions/download_docker_images.sh ghcr.io/github/gh-aw-firewall/agent:0.23.0 ghcr.io/github/gh-aw-firewall/api-proxy:0.23.0 ghcr.io/github/gh-aw-firewall/squid:0.23.0 ghcr.io/github/gh-aw-mcpg:v0.1.8 ghcr.io/github/github-mcp-server:v0.32.0 node:lts-alpine
- name: Write Safe Outputs Config
run: |
mkdir -p /opt/gh-aw/safeoutputs
@ -600,7 +603,7 @@ jobs:
"mcpServers": {
"github": {
"type": "stdio",
"container": "ghcr.io/github/github-mcp-server:v0.31.0",
"container": "ghcr.io/github/github-mcp-server:v0.32.0",
"env": {
"GITHUB_LOCKDOWN_MODE": "$GITHUB_MCP_LOCKDOWN",
"GITHUB_PERSONAL_ACCESS_TOKEN": "\${GITHUB_MCP_SERVER_TOKEN}",
@ -625,7 +628,7 @@ jobs:
}
GH_AW_MCP_CONFIG_EOF
- name: Download activation artifact
uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
uses: actions/download-artifact@70fc10c6e5e1ce46ad2ea6f2b72d43f7d47b13c3 # v8
with:
name: activation
path: /tmp/gh-aw
@ -637,6 +640,7 @@ jobs:
timeout-minutes: 90
run: |
set -o pipefail
touch /tmp/gh-aw/agent-step-summary.md
# shellcheck disable=SC1003
sudo -E awf --env-all --container-workdir "${GITHUB_WORKSPACE}" --allow-domains "api.business.githubcopilot.com,api.enterprise.githubcopilot.com,api.github.com,api.githubcopilot.com,api.individual.githubcopilot.com,api.snapcraft.io,archive.ubuntu.com,azure.archive.ubuntu.com,crl.geotrust.com,crl.globalsign.com,crl.identrust.com,crl.sectigo.com,crl.thawte.com,crl.usertrust.com,crl.verisign.com,crl3.digicert.com,crl4.digicert.com,crls.ssl.com,github.com,host.docker.internal,json-schema.org,json.schemastore.org,keyserver.ubuntu.com,ocsp.digicert.com,ocsp.geotrust.com,ocsp.globalsign.com,ocsp.identrust.com,ocsp.sectigo.com,ocsp.ssl.com,ocsp.thawte.com,ocsp.usertrust.com,ocsp.verisign.com,packagecloud.io,packages.cloud.google.com,packages.microsoft.com,ppa.launchpad.net,raw.githubusercontent.com,registry.npmjs.org,s.symcb.com,s.symcd.com,security.ubuntu.com,telemetry.enterprise.githubcopilot.com,ts-crl.ws.symantec.com,ts-ocsp.ws.symantec.com" --log-level info --proxy-logs-dir /tmp/gh-aw/sandbox/firewall/logs --enable-host-access --image-tag 0.23.0 --skip-pull --enable-api-proxy \
-- /bin/bash -c '/usr/local/bin/copilot --add-dir /tmp/gh-aw/ --log-level all --log-dir /tmp/gh-aw/sandbox/agent/logs/ --add-dir "${GITHUB_WORKSPACE}" --disable-builtin-mcps --allow-all-tools --allow-all-paths --prompt "$(cat /tmp/gh-aw/aw-prompts/prompt.txt)"' 2>&1 | tee -a /tmp/gh-aw/agent-stdio.log
@ -645,15 +649,22 @@ jobs:
COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
COPILOT_MODEL: ${{ vars.GH_AW_MODEL_AGENT_COPILOT || '' }}
GH_AW_MCP_CONFIG: /home/runner/.copilot/mcp-config.json
GH_AW_PHASE: agent
GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
GH_AW_SAFE_OUTPUTS: ${{ env.GH_AW_SAFE_OUTPUTS }}
GH_AW_VERSION: v0.57.2
GITHUB_API_URL: ${{ github.api_url }}
GITHUB_AW: true
GITHUB_HEAD_REF: ${{ github.head_ref }}
GITHUB_MCP_SERVER_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN || secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
GITHUB_REF_NAME: ${{ github.ref_name }}
GITHUB_SERVER_URL: ${{ github.server_url }}
GITHUB_STEP_SUMMARY: ${{ env.GITHUB_STEP_SUMMARY }}
GITHUB_STEP_SUMMARY: /tmp/gh-aw/agent-step-summary.md
GITHUB_WORKSPACE: ${{ github.workspace }}
GIT_AUTHOR_EMAIL: github-actions[bot]@users.noreply.github.com
GIT_AUTHOR_NAME: github-actions[bot]
GIT_COMMITTER_EMAIL: github-actions[bot]@users.noreply.github.com
GIT_COMMITTER_NAME: github-actions[bot]
XDG_CONFIG_HOME: /home/runner
- name: Detect inference access error
id: detect-inference-error
@ -713,9 +724,12 @@ jobs:
SECRET_GH_AW_GITHUB_MCP_SERVER_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN }}
SECRET_GH_AW_GITHUB_TOKEN: ${{ secrets.GH_AW_GITHUB_TOKEN }}
SECRET_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- name: Append agent step summary
if: always()
run: bash /opt/gh-aw/actions/append_agent_step_summary.sh
- name: Upload Safe Outputs
if: always()
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7
with:
name: safe-output
path: ${{ env.GH_AW_SAFE_OUTPUTS }}
@ -737,13 +751,13 @@ jobs:
await main();
- name: Upload sanitized agent output
if: always() && env.GH_AW_AGENT_OUTPUT
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7
with:
name: agent-output
path: ${{ env.GH_AW_AGENT_OUTPUT }}
if-no-files-found: warn
- name: Upload engine output files
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7
with:
name: agent_outputs
path: |
@ -788,7 +802,7 @@ jobs:
- name: Upload agent artifacts
if: always()
continue-on-error: true
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7
with:
name: agent-artifacts
path: |
@ -834,7 +848,7 @@ jobs:
if: always() && steps.detection_guard.outputs.run_detection == 'true'
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
env:
WORKFLOW_NAME: "Qf S Benchmark"
WORKFLOW_NAME: "ZIPT String Solver Benchmark"
WORKFLOW_DESCRIPTION: "Run Z3 string solver benchmarks (seq vs nseq) on QF_S test suite from the c3 branch and post results as a GitHub discussion"
HAS_PATCH: ${{ steps.collect_output.outputs.has_patch }}
with:
@ -862,6 +876,7 @@ jobs:
timeout-minutes: 20
run: |
set -o pipefail
touch /tmp/gh-aw/agent-step-summary.md
# shellcheck disable=SC1003
sudo -E awf --env-all --container-workdir "${GITHUB_WORKSPACE}" --allow-domains "api.business.githubcopilot.com,api.enterprise.githubcopilot.com,api.github.com,api.githubcopilot.com,api.individual.githubcopilot.com,github.com,host.docker.internal,raw.githubusercontent.com,registry.npmjs.org,telemetry.enterprise.githubcopilot.com" --log-level info --proxy-logs-dir /tmp/gh-aw/sandbox/firewall/logs --enable-host-access --image-tag 0.23.0 --skip-pull --enable-api-proxy \
-- /bin/bash -c '/usr/local/bin/copilot --add-dir /tmp/gh-aw/ --log-level all --log-dir /tmp/gh-aw/sandbox/agent/logs/ --add-dir "${GITHUB_WORKSPACE}" --disable-builtin-mcps --allow-tool '\''shell(cat)'\'' --allow-tool '\''shell(grep)'\'' --allow-tool '\''shell(head)'\'' --allow-tool '\''shell(jq)'\'' --allow-tool '\''shell(ls)'\'' --allow-tool '\''shell(tail)'\'' --allow-tool '\''shell(wc)'\'' --prompt "$(cat /tmp/gh-aw/aw-prompts/prompt.txt)"' 2>&1 | tee -a /tmp/gh-aw/threat-detection/detection.log
@ -869,13 +884,20 @@ jobs:
COPILOT_AGENT_RUNNER_TYPE: STANDALONE
COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
COPILOT_MODEL: ${{ vars.GH_AW_MODEL_DETECTION_COPILOT || '' }}
GH_AW_PHASE: detection
GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt
GH_AW_VERSION: v0.57.2
GITHUB_API_URL: ${{ github.api_url }}
GITHUB_AW: true
GITHUB_HEAD_REF: ${{ github.head_ref }}
GITHUB_REF_NAME: ${{ github.ref_name }}
GITHUB_SERVER_URL: ${{ github.server_url }}
GITHUB_STEP_SUMMARY: ${{ env.GITHUB_STEP_SUMMARY }}
GITHUB_STEP_SUMMARY: /tmp/gh-aw/agent-step-summary.md
GITHUB_WORKSPACE: ${{ github.workspace }}
GIT_AUTHOR_EMAIL: github-actions[bot]@users.noreply.github.com
GIT_AUTHOR_NAME: github-actions[bot]
GIT_COMMITTER_EMAIL: github-actions[bot]@users.noreply.github.com
GIT_COMMITTER_NAME: github-actions[bot]
XDG_CONFIG_HOME: /home/runner
- name: Parse threat detection results
id: parse_detection_results
@ -889,7 +911,7 @@ jobs:
await main();
- name: Upload threat detection log
if: always() && steps.detection_guard.outputs.run_detection == 'true'
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7
with:
name: threat-detection.log
path: /tmp/gh-aw/threat-detection/detection.log
@ -935,13 +957,13 @@ jobs:
total_count: ${{ steps.missing_tool.outputs.total_count }}
steps:
- name: Setup Scripts
uses: github/gh-aw/actions/setup@7d1a2798f21c06247ce115b7c7b8ddd70c8d0dc3 # v0.59.0
uses: github/gh-aw/actions/setup@32b3a711a9ee97d38e3989c90af0385aff0066a7 # v0.57.2
with:
destination: /opt/gh-aw/actions
- name: Download agent output artifact
id: download-agent-output
continue-on-error: true
uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
uses: actions/download-artifact@70fc10c6e5e1ce46ad2ea6f2b72d43f7d47b13c3 # v8
with:
name: agent-output
path: /tmp/gh-aw/safeoutputs/
@ -957,7 +979,7 @@ jobs:
env:
GH_AW_AGENT_OUTPUT: ${{ env.GH_AW_AGENT_OUTPUT }}
GH_AW_NOOP_MAX: "1"
GH_AW_WORKFLOW_NAME: "Qf S Benchmark"
GH_AW_WORKFLOW_NAME: "ZIPT String Solver Benchmark"
with:
github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
script: |
@ -972,7 +994,7 @@ jobs:
GH_AW_AGENT_OUTPUT: ${{ env.GH_AW_AGENT_OUTPUT }}
GH_AW_MISSING_TOOL_CREATE_ISSUE: "true"
GH_AW_MISSING_TOOL_TITLE_PREFIX: "[missing tool]"
GH_AW_WORKFLOW_NAME: "Qf S Benchmark"
GH_AW_WORKFLOW_NAME: "ZIPT String Solver Benchmark"
with:
github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
script: |
@ -985,7 +1007,7 @@ jobs:
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
env:
GH_AW_AGENT_OUTPUT: ${{ env.GH_AW_AGENT_OUTPUT }}
GH_AW_WORKFLOW_NAME: "Qf S Benchmark"
GH_AW_WORKFLOW_NAME: "ZIPT String Solver Benchmark"
GH_AW_RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
GH_AW_AGENT_CONCLUSION: ${{ needs.agent.result }}
GH_AW_WORKFLOW_ID: "qf-s-benchmark"
@ -995,6 +1017,7 @@ jobs:
GH_AW_CREATE_DISCUSSION_ERRORS: ${{ needs.safe_outputs.outputs.create_discussion_errors }}
GH_AW_CREATE_DISCUSSION_ERROR_COUNT: ${{ needs.safe_outputs.outputs.create_discussion_error_count }}
GH_AW_GROUP_REPORTS: "false"
GH_AW_FAILURE_REPORT_AS_ISSUE: "true"
GH_AW_TIMEOUT_MINUTES: "90"
with:
github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
@ -1008,7 +1031,7 @@ jobs:
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8
env:
GH_AW_AGENT_OUTPUT: ${{ env.GH_AW_AGENT_OUTPUT }}
GH_AW_WORKFLOW_NAME: "Qf S Benchmark"
GH_AW_WORKFLOW_NAME: "ZIPT String Solver Benchmark"
GH_AW_RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
GH_AW_AGENT_CONCLUSION: ${{ needs.agent.result }}
GH_AW_NOOP_MESSAGE: ${{ steps.noop.outputs.noop_message }}
@ -1034,7 +1057,7 @@ jobs:
GH_AW_CALLER_WORKFLOW_ID: "${{ github.repository }}/qf-s-benchmark"
GH_AW_ENGINE_ID: "copilot"
GH_AW_WORKFLOW_ID: "qf-s-benchmark"
GH_AW_WORKFLOW_NAME: "Qf S Benchmark"
GH_AW_WORKFLOW_NAME: "ZIPT String Solver Benchmark"
outputs:
code_push_failure_count: ${{ steps.process_safe_outputs.outputs.code_push_failure_count }}
code_push_failure_errors: ${{ steps.process_safe_outputs.outputs.code_push_failure_errors }}
@ -1044,13 +1067,13 @@ jobs:
process_safe_outputs_temporary_id_map: ${{ steps.process_safe_outputs.outputs.temporary_id_map }}
steps:
- name: Setup Scripts
uses: github/gh-aw/actions/setup@7d1a2798f21c06247ce115b7c7b8ddd70c8d0dc3 # v0.59.0
uses: github/gh-aw/actions/setup@32b3a711a9ee97d38e3989c90af0385aff0066a7 # v0.57.2
with:
destination: /opt/gh-aw/actions
- name: Download agent output artifact
id: download-agent-output
continue-on-error: true
uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
uses: actions/download-artifact@70fc10c6e5e1ce46ad2ea6f2b72d43f7d47b13c3 # v8
with:
name: agent-output
path: /tmp/gh-aw/safeoutputs/
@ -1078,7 +1101,7 @@ jobs:
await main();
- name: Upload safe output items manifest
if: always()
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7
with:
name: safe-output-items
path: /tmp/safe-output-items.jsonl