From 6c0358206ac97cb6761a839f56c2e6308c5f070e Mon Sep 17 00:00:00 2001 From: joaomhmpereira Date: Wed, 20 Nov 2024 20:27:14 +0000 Subject: [PATCH] Add missing flag to scripts --- bench/eq3.sh | 14 +++++++------- bench/testcomp.sh | 12 ++++++------ 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/bench/eq3.sh b/bench/eq3.sh index 98a6e258..a8131654 100755 --- a/bench/eq3.sh +++ b/bench/eq3.sh @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/bench/testcomp.sh b/bench/testcomp.sh index b6b7543b..6ebd2be2 100755 --- a/bench/testcomp.sh +++ b/bench/testcomp.sh @@ -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 ##