Skip to content

Commit

Permalink
Add missing flag to scripts
Browse files Browse the repository at this point in the history
  • Loading branch information
joaomhmpereira authored and filipeom committed Nov 20, 2024
1 parent b2c6e2d commit 6c03582
Show file tree
Hide file tree
Showing 2 changed files with 13 additions and 13 deletions.
14 changes: 7 additions & 7 deletions bench/eq3.sh
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ eval $(opam env)
if [ -e "csvs_single/QF_FP_z3_solver.csv" ]; then
: # do nothing
else
python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_z3_solver --prover z3
python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_z3_solver --prover z3
fi

python3 run_benchmarks.py --multi -F QF_FP_paths.list --output-dir csvs_multi --output-filename QF_FP_z3 --prover smtml-z3
Expand All @@ -17,7 +17,7 @@ python3 run_benchmarks.py --multi -F QF_FP_paths.list --output-dir csvs_multi --
if [ -e "csvs_single/QF_FP_bitwuzla_solver.csv" ]; then
: # do nothing
else
python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_bitwuzla_solver --prover bitwuzla
python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_bitwuzla_solver --prover bitwuzla
fi

python3 run_benchmarks.py --multi -F QF_FP_paths.list --output-dir csvs_multi --output-filename QF_FP_bitwuzla_solver --prover bitwuzla
Expand All @@ -27,7 +27,7 @@ python3 run_benchmarks.py --multi -F QF_FP_paths.list --output-dir csvs_multi --
if [ -e "csvs_single/QF_LIA_z3_solver.csv" ]; then
: # do nothing
else
python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_z3_solver --prover z3
python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_z3_solver --prover z3
fi

python3 run_benchmarks.py --multi -F QF_LIA_paths.list --output-dir csvs_multi --output-filename QF_LIA_z3 --prover smtml-z3
Expand All @@ -37,7 +37,7 @@ python3 run_benchmarks.py --multi -F QF_LIA_paths.list --output-dir csvs_multi -
if [ -e "csvs_single/QF_BV_z3_solver.csv" ]; then
: # do nothing
else
python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_z3_solver --prover z3
python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_z3_solver --prover z3
fi

python3 run_benchmarks.py --multi -F QF_BV_paths.list --output-dir csvs_multi --output-filename QF_BV_z3 --prover smtml-z3
Expand All @@ -46,7 +46,7 @@ python3 run_benchmarks.py --multi -F QF_BV_paths.list --output-dir csvs_multi --
if [ -e "csvs_single/QF_BV_bitwuzla_solver.csv" ]; then
: # do nothing
else
python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_bitwuzla_solver --prover bitwuzla
python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_bitwuzla_solver --prover bitwuzla
fi

python3 run_benchmarks.py --multi -F QF_BV_paths.list --output-dir csvs_multi --output-filename QF_BV_bitwuzla_solver --prover bitwuzla
Expand All @@ -56,7 +56,7 @@ python3 run_benchmarks.py --multi -F QF_BV_paths.list --output-dir csvs_multi --
if [ -e "csvs_single/QF_S_z3_solver.csv" ]; then
: # do nothing
else
python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_z3_solver --prover z3
python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_z3_solver --prover z3
fi

python3 run_benchmarks.py --multi -F QF_S_paths.list --output-dir csvs_multi --output-filename QF_S_z3 --prover smtml-z3
Expand All @@ -66,7 +66,7 @@ python3 run_benchmarks.py --multi -F QF_S_paths.list --output-dir csvs_multi --o
if [ -e "csvs_single/QF_SLIA_z3_solver.csv" ]; then
: # do nothing
else
python3 run_benchmarks.py --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_z3_solver --prover z3
python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_z3_solver --prover z3
fi

python3 run_benchmarks.py --multi -F QF_SLIA_paths.list --output-dir csvs_multi --output-filename QF_SLIA_z3 --prover smtml-z3
Expand Down
12 changes: 6 additions & 6 deletions bench/testcomp.sh
Original file line number Diff line number Diff line change
Expand Up @@ -4,18 +4,18 @@ opam sw z3-bitwuzla
eval $(opam env)

#### array-examples ####
python3 run_benchmarks.py --dir smt-testcomp23/array-examples --output-dir csvs_single --output-filename array_examples_z3_solver --prover z3
python3 run_benchmarks.py --dir smt-testcomp23/array-examples --output-dir csvs_single --output-filename array_examples_z3 --prover smtml-z3
python3 run_benchmarks.py --single --dir smt-testcomp23/array-examples --output-dir csvs_single --output-filename array_examples_z3_solver --prover z3
python3 run_benchmarks.py --single --dir smt-testcomp23/array-examples --output-dir csvs_single --output-filename array_examples_z3 --prover smtml-z3
python3 run_benchmarks.py --multi -F array_examples_paths.list --output-dir csvs_multi --output-filename array_examples_z3 --prover smtml-z3

#### array-industry-pattern ####
python3 run_benchmarks.py --dir smt-testcomp23/array-industry-pattern --output-dir csvs_single --output-filename array_industry_pattern_z3_solver --prover z3
python3 run_benchmarks.py --dir smt-testcomp23/array-industry-pattern --output-dir csvs_single --output-filename array_industry_pattern_z3 --prover smtml-z3
python3 run_benchmarks.py --single --dir smt-testcomp23/array-industry-pattern --output-dir csvs_single --output-filename array_industry_pattern_z3_solver --prover z3
python3 run_benchmarks.py --single --dir smt-testcomp23/array-industry-pattern --output-dir csvs_single --output-filename array_industry_pattern_z3 --prover smtml-z3
python3 run_benchmarks.py --multi -F array_industry_pattern_paths.list --output-dir csvs_multi --output-filename array_industry_pattern_z3 --prover smtml-z3

#### eca-rers2018 ####
python3 run_benchmarks.py --dir smt-testcomp23/eca-rers2018 --output-dir csvs_single --output-filename eca_rers2018_z3_solver --prover z3
python3 run_benchmarks.py --dir smt-testcomp23/eca-rers2018 --output-dir csvs_single --output-filename eca_rers2018_z3 --prover smtml-z3
python3 run_benchmarks.py --single --dir smt-testcomp23/eca-rers2018 --output-dir csvs_single --output-filename eca_rers2018_z3_solver --prover z3
python3 run_benchmarks.py --single --dir smt-testcomp23/eca-rers2018 --output-dir csvs_single --output-filename eca_rers2018_z3 --prover smtml-z3
python3 run_benchmarks.py --multi -F eca_rers2018_paths.list --output-dir csvs_multi --output-filename eca_rers2018_z3 --prover smtml-z3

## Plots ##
Expand Down

0 comments on commit 6c03582

Please sign in to comment.