diff --git a/.github/workflows/eval.yml b/.github/workflows/eval.yml index 7060c9fa..7da2a58d 100644 --- a/.github/workflows/eval.yml +++ b/.github/workflows/eval.yml @@ -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 diff --git a/eval/eval.sh b/eval/eval.sh index 19952f00..22edbb3f 100755 --- a/eval/eval.sh +++ b/eval/eval.sh @@ -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