Skip to content

Commit

Permalink
Split further
Browse files Browse the repository at this point in the history
  • Loading branch information
JonasAlaif committed Jan 14, 2025
1 parent 79ff76f commit e514052
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 7 deletions.
23 changes: 18 additions & 5 deletions .github/workflows/eval.yml
Original file line number Diff line number Diff line change
Expand Up @@ -11,23 +11,36 @@ jobs:
matrix:
verifier:
- name: 'carbon'
args: 'lt carbon/silver/src/test/resources/capture_avoidance/'
tag: '-1'
- name: 'carbon'
args: 'ge carbon/silver/src/test/resources/capture_avoidance/'
tag: '-2'
- name: 'dafny'
args: 'lt dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency'
args: 'lt dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/11-'
tag: '-1'
- name: 'dafny'
args: 'eq dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency'
args: 'in dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/concurrency/11- dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/'
tag: '-2'
- name: 'dafny'
args: 'gt dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers'
args: 'ge dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/'
tag: '-3'
- name: 'fstar'
args: 'lt fstar/examples/'
tag: '-1'
- name: 'fstar'
args: 'ge fstar/examples/'
tag: '-2'
- name: 'silicon'
- name: 'smt-comp'
args: 'lt smt-comp/non-incremental'
args: 'lt smt-comp/incremental/QF_BVLRA/20240414-mapf_r/soc/coef_2/'
tag: '-1'
- name: 'smt-comp'
args: 'gt smt-comp/non-incremental'
args: 'in smt-comp/incremental/QF_BVLRA/20240414-mapf_r/soc/coef_2/ smt-comp/non-incremental/QF_SLIA/'
tag: '-2'
- name: 'smt-comp'
args: 'ge smt-comp/non-incremental/QF_SLIA/'
tag: '-3'
- name: 'verus'
runs-on: ubuntu-latest

Expand Down
5 changes: 3 additions & 2 deletions eval/eval.sh
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,9 @@ while read -r file; do
OUTPUT="$DIRNAME/data/${FILE%.*}"

[[ "$2" == "lt" && "$3" < "$FILE" ]] && continue || true
[[ "$2" == "gt" && "$3" > "$FILE" ]] && continue || true
[[ "$2" == "eq" && "${FILE#"$3/"}" == "${FILE}" ]] && continue || true
[[ "$2" == "ge" && "$3" > "$FILE" ]] && continue || true
[[ "$2" == "eq" && "${FILE#"$3"}" == "${FILE}" ]] && continue || true
[[ "$2" == "in" && ("$3" > "$FILE" || "$4" < "$FILE") ]] && continue || true
[ -s "$OUTPUT.data" ] && echo "[.log] EXISTS $FILE" && continue || true

# [ "$FILE" == "silicon/silver/src/test/resources/quantifiedpermissions/misc/functions-01.smt2" ] || continue
Expand Down

0 comments on commit e514052

Please sign in to comment.