diff --git a/bench/eq1.sh b/bench/eq1.sh
index 5d1bec2a..1bb7af3f 100755
--- a/bench/eq1.sh
+++ b/bench/eq1.sh
@@ -1,31 +1,118 @@
 #!/bin/sh
 
+TEMPLATE=./tmp.XXXXXXXXXX
+
+show_help() {
+  echo "Usage: $0 [-n VALUE] [--help]"
+  echo
+  echo "Options:"
+  echo "  -n VALUE   Number of benchmarks to run."
+  echo "  --help     Show this help message and exit."
+  exit 0
+}
+
+sample_benchmarks() {
+  src=$1
+  dst=$2
+  n=$3
+
+  echo "Sampling '$n' benchmarks from '$src' to '$dst'"
+  files=$(find $src -type f -name "*.smt2" | shuf -n $n)
+  for file in $files; do
+    cp $file $dst
+  done
+
+  return 0
+}
+
+QF_BV_DIR=./smt-comp/smtlib/non-incremental/QF_BV
+QF_FP_DIR=./smt-comp/smtlib/non-incremental/QF_FP
+QF_LIA_DIR=./smt-comp/smtlib/non-incremental/QF_LIA
+QF_SLIA_DIR=./smt-comp/smtlib/non-incremental/QF_SLIA
+QF_S_DIR=./smt-comp/smtlib/non-incremental/QF_S
+
+n_value=""
+dry_value=false
+
+while [[ $# -gt 0 ]]; do
+  case $1 in
+    -n)
+      shift
+      if [[ -z "$1" || "$1" == -* ]]; then
+        echo "Error: Missing value for -n option."
+        exit 1
+      fi
+      n_value=$1
+      shift
+      ;;
+    --dry)
+      dry_value=true
+      shift
+      ;;
+    --help)
+      show_help
+      ;;
+    *)
+      echo "Error: Unknown argument: $1"
+      show_help
+      ;;
+  esac
+done
+
+if [[ -n "$n_value" ]]; then
+  echo "Sampling $n_value benchmarks ..."
+  qf_bv=$(mktemp -d "$TEMPLATE")
+  sample_benchmarks "$QF_BV_DIR" "$qf_bv" "$n_value"
+  QF_BV_DIR="$qf_bv"
+
+  qf_fp=$(mktemp -d "$TEMPLATE")
+  sample_benchmarks "$QF_FP_DIR" "$qf_fp" "$n_value"
+  QF_FP_DIR="$qf_fp"
+
+  qf_lia=$(mktemp -d "$TEMPLATE")
+  sample_benchmarks "$QF_LIA_DIR" "$qf_lia" "$n_value"
+  QF_LIA_DIR="$qf_lia"
+
+  qf_slia=$(mktemp -d "$TEMPLATE")
+  sample_benchmarks "$QF_SLIA_DIR" "$qf_slia" "$n_value"
+  QF_SLIA_DIR="$qf_slia"
+
+  qf_s=$(mktemp -d "$TEMPLATE")
+  sample_benchmarks "$QF_S_DIR" "$qf_s" "$n_value"
+  QF_S_DIR="$qf_s"
+fi
+
+$dry_value && exit 0
+
 mkdir eq1
 
 opam sw z3-bitwuzla
 eval $(opam env)
 
 mkdir eq1/z3-bitwuzla
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_BV -p z3 -p smtml-z3 -p bitwuzla -p smtml-bitwuzla > eq1/z3-bitwuzla/qf_bv.out
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_FP -p z3 -p smtml-z3 -p bitwuzla -p smtml-bitwuzla > eq1/z3-bitwuzla/qf_fp.out
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_LIA -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_lia.out
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_SLIA -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_slia.out
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_S -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_s.out
+echo "Running Z3 and bitwuzla ..."
+benchpress run -c benchpress.sexp --task eq1 $QF_BV_DIR -p z3 -p smtml-z3 -p bitwuzla -p smtml-bitwuzla > eq1/z3-bitwuzla/qf_bv.out
+benchpress run -c benchpress.sexp --task eq1 $QF_FP_DIR -p z3 -p smtml-z3 -p bitwuzla -p smtml-bitwuzla > eq1/z3-bitwuzla/qf_fp.out
+benchpress run -c benchpress.sexp --task eq1 $QF_LIA_DIR -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_lia.out
+benchpress run -c benchpress.sexp --task eq1 $QF_SLIA_DIR -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_slia.out
+benchpress run -c benchpress.sexp --task eq1 $QF_S_DIR -p z3 -p smtml-z3 > eq1/z3-bitwuzla/qf_s.out
 
 opam sw cvc5
 eval $(opam env)
 
 mkdir eq1/cvc5
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_BV -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_bv.out
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_FP -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_fp.out
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_LIA -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_lia.out
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_SLIA -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_slia.out
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_S -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_s.out
+echo "Running cvc5 ..."
+benchpress run -c benchpress.sexp --task eq1 $QF_BV_DIR -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_bv.out
+benchpress run -c benchpress.sexp --task eq1 $QF_FP_DIR -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_fp.out
+benchpress run -c benchpress.sexp --task eq1 $QF_LIA_DIR -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_lia.out
+benchpress run -c benchpress.sexp --task eq1 $QF_SLIA_DIR -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_slia.out
+benchpress run -c benchpress.sexp --task eq1 $QF_S_DIR -p cvc5 -p smtml-cvc5 > eq1/cvc5/qf_s.out
 
 opam sw colibri2
 eval $(opam env)
 
 mkdir eq1/colibri2
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_BV -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_bv.out
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_FP -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_fp.out
-benchpress run -c benchpress.sexp --task eq1 ./smt-comp/smtlib/non-incremental/QF_LIA -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_lia.out
+echo "Running Colibri2 ..."
+benchpress run -c benchpress.sexp --task eq1 $QF_BV_DIR -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_bv.out
+benchpress run -c benchpress.sexp --task eq1 $QF_FP_DIR -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_fp.out
+benchpress run -c benchpress.sexp --task eq1 $QF_LIA_DIR -p colibri2 -p smtml-colibri2 > eq1/colibri2/qf_lia.out
diff --git a/bench/eq2.sh b/bench/eq2.sh
index 4cf741a4..abadb706 100755
--- a/bench/eq2.sh
+++ b/bench/eq2.sh
@@ -1,73 +1,201 @@
 #!/bin/bash
 
+TEMPLATE=./tmp.XXXXXXXXXX
+
+show_help() {
+  echo "Usage: $0 [-n VALUE] [--help]"
+  echo
+  echo "Options:"
+  echo "  -n VALUE   Number of benchmarks to run."
+  echo "  --help     Show this help message and exit."
+  exit 0
+}
+
+sample_benchmarks() {
+  src=$1
+  dst=$2
+  n=$3
+
+  echo "Sampling '$n' benchmarks from '$src' to '$dst'"
+  files=$(find $src -type f -name "*.smt2" | shuf -n $n)
+  for file in $files; do
+    cp $file $dst
+  done
+
+  return 0
+}
+
+QF_BV_DIR=./smt-comp/smtlib/non-incremental/QF_BV
+QF_FP_DIR=./smt-comp/smtlib/non-incremental/QF_FP
+QF_LIA_DIR=./smt-comp/smtlib/non-incremental/QF_LIA
+QF_SLIA_DIR=./smt-comp/smtlib/non-incremental/QF_SLIA
+QF_S_DIR=./smt-comp/smtlib/non-incremental/QF_S
+
+n_value=""
+dry_value=false
+
+while [[ $# -gt 0 ]]; do
+  case $1 in
+    -n)
+      shift
+      if [[ -z "$1" || "$1" == -* ]]; then
+        echo "Error: Missing value for -n option."
+        exit 1
+      fi
+      n_value=$1
+      shift
+      ;;
+    --dry)
+      dry_value=true
+      shift
+      ;;
+    --help)
+      show_help
+      ;;
+    *)
+      echo "Error: Unknown argument: $1"
+      show_help
+      ;;
+  esac
+done
+
+if [[ -n "$n_value" ]]; then
+  echo "Sampling $n_value benchmarks ..."
+  qf_bv=$(mktemp -d "$TEMPLATE")
+  sample_benchmarks "$QF_BV_DIR" "$qf_bv" "$n_value"
+  QF_BV_DIR="$qf_bv"
+
+  qf_fp=$(mktemp -d "$TEMPLATE")
+  sample_benchmarks "$QF_FP_DIR" "$qf_fp" "$n_value"
+  QF_FP_DIR="$qf_fp"
+
+  qf_lia=$(mktemp -d "$TEMPLATE")
+  sample_benchmarks "$QF_LIA_DIR" "$qf_lia" "$n_value"
+  QF_LIA_DIR="$qf_lia"
+
+  qf_slia=$(mktemp -d "$TEMPLATE")
+  sample_benchmarks "$QF_SLIA_DIR" "$qf_slia" "$n_value"
+  QF_SLIA_DIR="$qf_slia"
+
+  qf_s=$(mktemp -d "$TEMPLATE")
+  sample_benchmarks "$QF_S_DIR" "$qf_s" "$n_value"
+  QF_S_DIR="$qf_s"
+fi
+
+$dry_value && exit 0
+
 ## Z3 and Bitwuzla ##
 opam sw z3-bitwuzla
 eval $(opam env)
 #### QF_FP ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_z3 --prover smtml-z3
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_bitwuzla --prover smtml-bitwuzla
-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
-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
+echo "Running Z3 and bitwuzla ..."
+python3 run_benchmarks.py --single --dir $QF_FP_DIR --output-dir csvs_single --output-filename QF_FP_z3 --prover smtml-z3
+python3 run_benchmarks.py --single --dir $QF_FP_DIR --output-dir csvs_single --output-filename QF_FP_bitwuzla --prover smtml-bitwuzla
+python3 run_benchmarks.py --single --dir $QF_FP_DIR --output-dir csvs_single --output-filename QF_FP_z3_solver --prover z3
+python3 run_benchmarks.py --single --dir $QF_FP_DIR --output-dir csvs_single --output-filename QF_FP_bitwuzla_solver --prover bitwuzla
 #### QF_LIA ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_z3 --prover smtml-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
+python3 run_benchmarks.py --single --dir $QF_LIA_DIR --output-dir csvs_single --output-filename QF_LIA_z3 --prover smtml-z3
+python3 run_benchmarks.py --single --dir $QF_LIA_DIR --output-dir csvs_single --output-filename QF_LIA_z3_solver --prover z3
 #### QF_BV ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_z3 --prover smtml-z3
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_bitwuzla --prover smtml-bitwuzla
-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
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_bitwuzla --prover smtml-bitwuzla
+python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_z3 --prover smtml-z3
+python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_bitwuzla --prover smtml-bitwuzla
+python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_z3_solver --prover z3
+python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_bitwuzla --prover smtml-bitwuzla
 #### QF_S ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_z3 --prover smtml-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
+python3 run_benchmarks.py --single --dir $QF_S_DIR --output-dir csvs_single --output-filename QF_S_z3 --prover smtml-z3
+python3 run_benchmarks.py --single --dir $QF_S_DIR --output-dir csvs_single --output-filename QF_S_z3_solver --prover z3
 #### QF_SLIA ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_z3 --prover smtml-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
+python3 run_benchmarks.py --single --dir $QF_SLIA_DIR --output-dir csvs_single --output-filename QF_SLIA_z3 --prover smtml-z3
+python3 run_benchmarks.py --single --dir $QF_SLIA_DIR --output-dir csvs_single --output-filename QF_SLIA_z3_solver --prover z3
 
 ## cvc5 ##
 opam sw cvc5
 eval $(opam env)
+echo "Running cvc5 ..."
 #### QF_FP ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_cvc5 --prover smtml-cvc5
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_cvc5_solver --prover cvc5
+python3 run_benchmarks.py --single --dir $QF_FP_DIR --output-dir csvs_single --output-filename QF_FP_cvc5 --prover smtml-cvc5
+python3 run_benchmarks.py --single --dir $QF_FP_DIR --output-dir csvs_single --output-filename QF_FP_cvc5_solver --prover cvc5
 #### QF_LIA ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_cvc5 --prover smtml-cvc5
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_cvc5_solver --prover cvc5
+python3 run_benchmarks.py --single --dir $QF_LIA_DIR --output-dir csvs_single --output-filename QF_LIA_cvc5 --prover smtml-cvc5
+python3 run_benchmarks.py --single --dir $QF_LIA_DIR --output-dir csvs_single --output-filename QF_LIA_cvc5_solver --prover cvc5
 #### QF_BV ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_cvc5 --prover smtml-cvc5
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_cvc5_solver --prover cvc5
+python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_cvc5 --prover smtml-cvc5
+python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_cvc5_solver --prover cvc5
 #### QF_S ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_cvc5 --prover smtml-cvc5
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_S --output-dir csvs_single --output-filename QF_S_cvc5_solver --prover cvc5
+python3 run_benchmarks.py --single --dir $QF_S_DIR --output-dir csvs_single --output-filename QF_S_cvc5 --prover smtml-cvc5
+python3 run_benchmarks.py --single --dir $QF_S_DIR --output-dir csvs_single --output-filename QF_S_cvc5_solver --prover cvc5
 #### QF_SLIA ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_cvc5 --prover smtml-cvc5
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_SLIA --output-dir csvs_single --output-filename QF_SLIA_cvc5_solver --prover cvc5
+python3 run_benchmarks.py --single --dir $QF_SLIA_DIR --output-dir csvs_single --output-filename QF_SLIA_cvc5 --prover smtml-cvc5
+python3 run_benchmarks.py --single --dir $QF_SLIA_DIR --output-dir csvs_single --output-filename QF_SLIA_cvc5_solver --prover cvc5
 
 ## Colibri2 ##
 opam sw colibri2
 eval $(opam env)
+echo "Running Colibri2 ..."
 #### QF_FP ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_colibri2 --prover smtml-colibri2
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_FP --output-dir csvs_single --output-filename QF_FP_colibri2_solver --prover colibri2
+python3 run_benchmarks.py --single --dir $QF_FP_DIR --output-dir csvs_single --output-filename QF_FP_colibri2 --prover smtml-colibri2
+python3 run_benchmarks.py --single --dir $QF_FP_DIR --output-dir csvs_single --output-filename QF_FP_colibri2_solver --prover colibri2
 #### QF_LIA ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_colibri2 --prover smtml-colibri2
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_LIA --output-dir csvs_single --output-filename QF_LIA_colibri2_solver --prover colibri2
+python3 run_benchmarks.py --single --dir $QF_LIA_DIR --output-dir csvs_single --output-filename QF_LIA_colibri2 --prover smtml-colibri2
+python3 run_benchmarks.py --single --dir $QF_LIA_DIR --output-dir csvs_single --output-filename QF_LIA_colibri2_solver --prover colibri2
 #### QF_BV ####
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_colibri2 --prover smtml-colibri2
-python3 run_benchmarks.py --single --dir smt-comp/smtlib/non-incremental/QF_BV --output-dir csvs_single --output-filename QF_BV_colibri2_solver --prover colibri2
+python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_colibri2 --prover smtml-colibri2
+python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_colibri2_solver --prover colibri2
 
 ## Concat CSVs ##
+echo "Concatenating csvs ..."
 #### QF_FP ####
-python3 plots.py --output csvs_single/QF_FP_all.csv --concat --files csvs_single/QF_FP_z3.csv csvs_single/QF_FP_bitwuzla.csv csvs_single/QF_FP_cvc5.csv csvs_single/QF_FP_colibri2.csv csvs_single/QF_FP_z3_solver.csv csvs_single/QF_FP_bitwuzla_solver.csv csvs_single/QF_FP_cvc5_solver.csv csvs_single/QF_FP_colibri2_solver.csv
+python3 plots.py --output csvs_single/QF_FP_all.csv \
+  --concat \
+  --files \
+  csvs_single/QF_FP_z3.csv \
+  csvs_single/QF_FP_bitwuzla.csv \
+  csvs_single/QF_FP_cvc5.csv \
+  csvs_single/QF_FP_colibri2.csv \
+  csvs_single/QF_FP_z3_solver.csv \
+  csvs_single/QF_FP_bitwuzla_solver.csv \
+  csvs_single/QF_FP_cvc5_solver.csv \
+  csvs_single/QF_FP_colibri2_solver.csv
 #### QF_LIA ####
-python3 plots.py --output csvs_single/QF_LIA_all.csv --concat --files csvs_single/QF_LIA_z3.csv csvs_single/QF_LIA_cvc5.csv csvs_single/QF_LIA_colibri2.csv csvs_single/QF_LIA_z3_solver.csv csvs_single/QF_LIA_cvc5_solver.csv csvs_single/QF_LIA_colibri2_solver.csv
+python3 plots.py --output csvs_single/QF_LIA_all.csv \
+  --concat \
+  --files \
+  csvs_single/QF_LIA_z3.csv \
+  csvs_single/QF_LIA_cvc5.csv \
+  csvs_single/QF_LIA_colibri2.csv \
+  csvs_single/QF_LIA_z3_solver.csv \
+  csvs_single/QF_LIA_cvc5_solver.csv \
+  csvs_single/QF_LIA_colibri2_solver.csv
 #### QF_BV ####
-python3 plots.py --output csvs_single/QF_BV_all.csv --concat --files csvs_single/QF_BV_z3.csv csvs_single/QF_BV_bitwuzla.csv csvs_single/QF_BV_cvc5.csv csvs_single/QF_BV_colibri2.csv csvs_single/QF_BV_z3_solver.csv csvs_single/QF_BV_bitwuzla_solver.csv csvs_single/QF_BV_cvc5_solver.csv csvs_single/QF_BV_colibri2_solver.csv
+python3 plots.py --output csvs_single/QF_BV_all.csv \
+  --concat \
+  --files \
+  csvs_single/QF_BV_z3.csv \
+  csvs_single/QF_BV_bitwuzla.csv \
+  csvs_single/QF_BV_cvc5.csv \
+  csvs_single/QF_BV_colibri2.csv \
+  csvs_single/QF_BV_z3_solver.csv \
+  csvs_single/QF_BV_bitwuzla_solver.csv \
+  csvs_single/QF_BV_cvc5_solver.csv \
+  csvs_single/QF_BV_colibri2_solver.csv
 #### QF_S ####
-python3 plots.py --output csvs_single/QF_S_all.csv --concat --files csvs_single/QF_S_z3.csv csvs_single/QF_S_cvc5.csv csvs_single/QF_S_z3_solver.csv csvs_single/QF_S_cvc5_solver.csv
+python3 plots.py --output csvs_single/QF_S_all.csv \
+  --concat \
+  --files \
+  csvs_single/QF_S_z3.csv \
+  csvs_single/QF_S_cvc5.csv \
+  csvs_single/QF_S_z3_solver.csv \
+  csvs_single/QF_S_cvc5_solver.csv
 #### QF_SLIA ####
-python3 plots.py --output csvs_single/QF_SLIA_all.csv --concat --files csvs_single/QF_SLIA_z3.csv csvs_single/QF_SLIA_cvc5.csv csvs_single/QF_SLIA_z3_solver.csv csvs_single/QF_SLIA_cvc5_solver.csv
+python3 plots.py --output csvs_single/QF_SLIA_all.csv \
+  --concat \
+  --files csvs_single/QF_SLIA_z3.csv \
+  csvs_single/QF_SLIA_cvc5.csv \
+  csvs_single/QF_SLIA_z3_solver.csv \
+  csvs_single/QF_SLIA_cvc5_solver.csv
 
 ## Generate plots ##
+echo "Generating plots ..."
 #### QF_FP ####
 python3 plots.py --single --QF-FP --output plot_QF_FP --files csvs_single/QF_FP_all.csv
 #### QF_LIA ####
@@ -77,4 +205,4 @@ python3 plots.py --single --QF-BV --output plot_QF_BV --files csvs_single/QF_BV_
 #### QF_S ####
 python3 plots.py --single --QF-S --output plot_QF_S --files csvs_single/QF_S_all.csv
 #### QF_SLIA ####
-python3 plots.py --single --QF-SLIA --output plot_QF_SLIA --files csvs_single/QF_SLIA_all.csv
\ No newline at end of file
+python3 plots.py --single --QF-SLIA --output plot_QF_SLIA --files csvs_single/QF_SLIA_all.csv
diff --git a/bench/eq3.sh b/bench/eq3.sh
index a8131654..02f2a944 100755
--- a/bench/eq3.sh
+++ b/bench/eq3.sh
@@ -1,5 +1,132 @@
 #!/bin/bash
 
+TEMPLATE=./tmp.XXXXXXXXXX
+
+show_help() {
+  echo "Usage: $0 [-n VALUE] [--help]"
+  echo
+  echo "Options:"
+  echo "  -n VALUE   Number of benchmarks to run."
+  echo "  --help     Show this help message and exit."
+  exit 0
+}
+
+sample_dir_benchmarks() {
+  src=$1
+  dst=$2
+  n=$3
+
+  echo "Sampling '$n' benchmarks from '$src' to '$dst'"
+  files=$(find $src -type f -name "*.smt2" | shuf -n $n)
+  for file in $files; do
+    cp $file $dst
+  done
+
+  return 0
+}
+
+sample_list_benchmarks() {
+  src=$1
+  output=$2
+  n=$3
+
+  echo "Sampling '$n' benchmarks listed in '$src' to '$output'"
+
+  if [[ ! -f $src ]]; then
+    echo "Error: Source file '$src' does not exist."
+    return 1
+  fi
+
+  sampled=$(shuf -n $n "$src")
+
+  echo "$sampled" > "$output"
+
+  return 0
+}
+
+QF_BV_DIR=./smt-comp/smtlib/non-incremental/QF_BV
+QF_BV_LIST=./QF_BV_paths.list
+
+QF_FP_DIR=./smt-comp/smtlib/non-incremental/QF_FP
+QF_FP_LIST=./QF_FP_paths.list
+
+QF_LIA_DIR=./smt-comp/smtlib/non-incremental/QF_LIA
+QF_LIA_LIST=./QF_LIA_paths.list
+
+QF_SLIA_DIR=./smt-comp/smtlib/non-incremental/QF_SLIA
+QF_SLIA_LIST=./QF_SLIA_paths.list
+
+QF_S_DIR=./smt-comp/smtlib/non-incremental/QF_S
+QF_S_LIST=./QF_S_paths.list
+
+n_value=""
+dry_value=false
+
+while [[ $# -gt 0 ]]; do
+  case $1 in
+    -n)
+      shift
+      if [[ -z "$1" || "$1" == -* ]]; then
+        echo "Error: Missing value for -n option."
+        exit 1
+      fi
+      n_value=$1
+      shift
+      ;;
+    --dry)
+      dry_value=true
+      shift
+      ;;
+    --help)
+      show_help
+      ;;
+    *)
+      echo "Error: Unknown argument: $1"
+      show_help
+      ;;
+  esac
+done
+
+if [[ -n "$n_value" ]]; then
+  echo "Sampling $n_value benchmarks ..."
+  qf_bv=$(mktemp -d "$TEMPLATE")
+  qf_bv_list=$(mktemp "$TEMPLATE")
+  sample_dir_benchmarks "$QF_BV_DIR" "$qf_bv" "$n_value"
+  sample_list_benchmarks "$QF_BV_LIST" "$qf_bv_list" "$n_value"
+  QF_BV_DIR="$qf_bv"
+  QF_BV_LIST="$qf_bv_list"
+
+  qf_fp=$(mktemp -d "$TEMPLATE")
+  qf_fp_list=$(mktemp "$TEMPLATE")
+  sample_dir_benchmarks "$QF_FP_DIR" "$qf_fp" "$n_value"
+  sample_list_benchmarks "$QF_FP_LIST" "$qf_fp_list" "$n_value"
+  QF_FP_DIR="$qf_fp"
+  QF_FP_LIST="$qf_fp_list"
+
+  qf_lia=$(mktemp -d "$TEMPLATE")
+  qf_lia_list=$(mktemp "$TEMPLATE")
+  sample_dir_benchmarks "$QF_LIA_DIR" "$qf_lia" "$n_value"
+  sample_list_benchmarks "$QF_LIA_LIST" "$qf_lia_list" "$n_value"
+  QF_LIA_DIR="$qf_lia"
+  QF_LIA_LIST="$qf_lia_list"
+
+  qf_slia=$(mktemp -d "$TEMPLATE")
+  qf_slia_list=$(mktemp "$TEMPLATE")
+  sample_dir_benchmarks "$QF_SLIA_DIR" "$qf_slia" "$n_value"
+  sample_list_benchmarks "$QF_SLIA_LIST" "$qf_slia_list" "$n_value"
+  QF_SLIA_DIR="$qf_slia"
+  QF_SLIA_LIST="$qf_slia_list"
+
+  qf_s=$(mktemp -d "$TEMPLATE")
+  qf_s_list=$(mktemp "$TEMPLATE")
+  sample_dir_benchmarks "$QF_S_DIR" "$qf_s" "$n_value"
+  sample_list_benchmarks "$QF_S_LIST" "$qf_s_list" "$n_value"
+  QF_S_DIR="$qf_s"
+  QF_S_LIST="$qf_s_list"
+fi
+
+$dry_value && exit 0
+
 opam sw z3-bitwuzla
 eval $(opam env)
 
@@ -8,83 +135,102 @@ eval $(opam env)
 if [ -e "csvs_single/QF_FP_z3_solver.csv" ]; then
   : # do nothing
 else
-  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
+  python3 run_benchmarks.py --single --dir $QF_FP_DIR --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
+python3 run_benchmarks.py --multi -F $QF_FP_LIST --output-dir csvs_multi --output-filename QF_FP_z3 --prover smtml-z3
 
 ## Bitwuzla ##
 if [ -e "csvs_single/QF_FP_bitwuzla_solver.csv" ]; then
   : # do nothing
 else
-  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
+  python3 run_benchmarks.py --single --dir $QF_FP_DIR --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
+python3 run_benchmarks.py --multi -F $QF_FP_LIST --output-dir csvs_multi --output-filename QF_FP_bitwuzla_solver --prover bitwuzla
 
 #### QF_LIA ####
 ## Z3 ##
 if [ -e "csvs_single/QF_LIA_z3_solver.csv" ]; then
   : # do nothing
 else
-  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
+  python3 run_benchmarks.py --single --dir $QF_LIA_DIR --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
+python3 run_benchmarks.py --multi -F $QF_LIA_LIST --output-dir csvs_multi --output-filename QF_LIA_z3 --prover smtml-z3
 
 #### QF_BV ####
 ## Z3 ##
 if [ -e "csvs_single/QF_BV_z3_solver.csv" ]; then
   : # do nothing
 else
-  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
+  python3 run_benchmarks.py --single --dir $QF_BV_DIR --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
+python3 run_benchmarks.py --multi -F $QF_BV_LIST --output-dir csvs_multi --output-filename QF_BV_z3 --prover smtml-z3
 
 ## Bitwuzla ##
 if [ -e "csvs_single/QF_BV_bitwuzla_solver.csv" ]; then
   : # do nothing
 else
-  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
+  python3 run_benchmarks.py --single --dir $QF_BV_DIR --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
+python3 run_benchmarks.py --multi -F $QF_BV_LIST --output-dir csvs_multi --output-filename QF_BV_bitwuzla_solver --prover bitwuzla
 
 #### QF_S ####
 ## Z3 ##
 if [ -e "csvs_single/QF_S_z3_solver.csv" ]; then
   : # do nothing
 else
-  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
+  python3 run_benchmarks.py --single --dir $QF_S_DIR --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
+python3 run_benchmarks.py --multi -F $QF_S_LIST --output-dir csvs_multi --output-filename QF_S_z3 --prover smtml-z3
 
 #### QF_SLIA ####
 ## Z3 ##
 if [ -e "csvs_single/QF_SLIA_z3_solver.csv" ]; then
   : # do nothing
 else
-  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
+  python3 run_benchmarks.py --single --dir $QF_SLIA_DIR --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
+python3 run_benchmarks.py --multi -F $QF_SLIA_LIST --output-dir csvs_multi --output-filename QF_SLIA_z3 --prover smtml-z3
 
 
 ## Generate plots ##
 
 ## QF_FP ##
-python3 plots.py --multi --QF-FP --output plot_QF_FP_multi --files csvs_multi/QF_FP_z3.csv csvs_multi/QF_FP_bitwuzla.csv csvs_single/QF_FP_z3_solver.csv csvs_single/QF_FP_bitwuzla_solver.csv
+python3 plots.py --multi --QF-FP --output plot_QF_FP_multi \
+  --files \
+  csvs_multi/QF_FP_z3.csv \
+  csvs_multi/QF_FP_bitwuzla.csv \
+  csvs_single/QF_FP_z3_solver.csv \
+  csvs_single/QF_FP_bitwuzla_solver.csv
 
 ## QF_LIA ##
-python3 plots.py --multi --QF-LIA --output plot_QF_LIA_multi --files csvs_multi/QF_LIA_z3.csv csvs_single/QF_LIA_z3_solver.csv
+python3 plots.py --multi --QF-LIA --output plot_QF_LIA_multi \
+  --files \
+  csvs_multi/QF_LIA_z3.csv \
+  csvs_single/QF_LIA_z3_solver.csv
 
 ## QF_BV ##
-python3 plots.py --multi --QF-BV --output plot_QF_BV_multi --files csvs_multi/QF_BV_z3.csv csvs_multi/QF_BV_bitwuzla.csv csvs_single/QF_BV_z3_solver.csv csvs_single/QF_BV_bitwuzla_solver.csv
+python3 plots.py --multi --QF-BV --output plot_QF_BV_multi \
+  --files \
+  csvs_multi/QF_BV_z3.csv \
+  csvs_multi/QF_BV_bitwuzla.csv \
+  csvs_single/QF_BV_z3_solver.csv \
+  csvs_single/QF_BV_bitwuzla_solver.csv
 
 ## QF_S ##
-python3 plots.py --multi --QF-S --output plot_QF_S_multi --files csvs_multi/QF_S_z3.csv csvs_single/QF_S_z3_solver.csv
+python3 plots.py --multi --QF-S --output plot_QF_S_multi \
+  --files \
+  csvs_multi/QF_S_z3.csv \
+  csvs_single/QF_S_z3_solver.csv
 
 ## QF_SLIA ##
-python3 plots.py --multi --QF-SLIA --output plot_QF_SLIA_multi --files csvs_multi/QF_SLIA_z3.csv csvs_single/QF_SLIA_z3_solver.csv
\ No newline at end of file
+python3 plots.py --multi --QF-SLIA --output plot_QF_SLIA_multi \
+  --files \
+  csvs_multi/QF_SLIA_z3.csv \
+  csvs_single/QF_SLIA_z3_solver.csv
diff --git a/bench/testcomp.sh b/bench/testcomp.sh
index 6ebd2be2..76e50308 100755
--- a/bench/testcomp.sh
+++ b/bench/testcomp.sh
@@ -1,24 +1,177 @@
 #!/bin/bash
 
+TEMPLATE=./tmp.XXXXXXXXXX
+
+show_help() {
+  echo "Usage: $0 [-n VALUE] [--help]"
+  echo
+  echo "Options:"
+  echo "  -n VALUE   Number of benchmarks to run."
+  echo "  --help     Show this help message and exit."
+  exit 0
+}
+
+sample_dir_benchmarks() {
+  src=$1
+  dst=$2
+  n=$3
+
+  echo "Sampling '$n' benchmarks from '$src' to '$dst'"
+  files=$(find $src -type f -name "*.smt2" | shuf -n $n)
+  for file in $files; do
+    cp $file $dst
+  done
+
+  return 0
+}
+
+sample_list_benchmarks() {
+  src=$1
+  output=$2
+  n=$3
+
+  echo "Sampling '$n' benchmarks listed in '$src' to '$output'"
+
+  if [[ ! -f $src ]]; then
+    echo "Error: Source file '$src' does not exist."
+    return 1
+  fi
+
+  sampled=$(shuf -n $n "$src")
+
+  echo "$sampled" > "$output"
+
+  return 0
+}
+
+ARRAY_EXAMPLES_DIR=./smt-testcomp23/array-examples
+ARRAY_EXAMPLES_LIST=./array_examples_paths.list
+
+ARRAY_INDUSTRY_DIR=./smt-testcomp23/array-industry-pattern
+ARRAY_INDUSTRY_LIST=./array_industry_pattern_paths.list
+
+ECA_DIR=./smt-testcomp23/eca-rers2018
+ECA_LIST=./eca_rers2018_paths.list
+
+n_value=""
+dry_value=false
+
+while [[ $# -gt 0 ]]; do
+  case $1 in
+    -n)
+      shift
+      if [[ -z "$1" || "$1" == -* ]]; then
+        echo "Error: Missing value for -n option."
+        exit 1
+      fi
+      n_value=$1
+      shift
+      ;;
+    --dry)
+      dry_value=true
+      shift
+      ;;
+    --help)
+      show_help
+      ;;
+    *)
+      echo "Error: Unknown argument: $1"
+      show_help
+      ;;
+  esac
+done
+
+if [[ -n "$n_value" ]]; then
+  echo "Sampling $n_value benchmarks ..."
+  array_examples=$(mktemp -d "$TEMPLATE")
+  array_examples_list=$(mktemp "$TEMPLATE")
+  sample_dir_benchmarks "$ARRAY_EXAMPLES_DIR" "$array_examples" "$n_value"
+  sample_list_benchmarks "$ARRAY_EXAMPLES_LIST" "$array_examples_list" "$n_value"
+  ARRAY_EXAMPLES_DIR="$array_examples"
+  ARRAY_EXAMPLES_LIST="$array_examples_list"
+
+  array_industry=$(mktemp -d "$TEMPLATE")
+  array_industry_list=$(mktemp "$TEMPLATE")
+  sample_dir_benchmarks "$ARRAY_INDUSTRY_DIR" "$array_industry" "$n_value"
+  sample_list_benchmarks "$ARRAY_INDUSTRY_LIST" "$array_industry_list" "$n_value"
+  ARRAY_INDUSTRY_DIR="$array_industry"
+  ARRAY_INDUSTRY_LIST="$array_industry_list"
+
+  eca_dir=$(mktemp -d "$TEMPLATE")
+  eca_list=$(mktemp "$TEMPLATE")
+  sample_dir_benchmarks "$ECA_DIR" "$eca_dir" "$n_value"
+  sample_list_benchmarks "$ECA_LIST" "$eca_list" "$n_value"
+  ECA_DIR="$eca_dir"
+  ECA_LIST="$eca_list"
+fi
+
+$dry_value && exit 0
+
 opam sw z3-bitwuzla
 eval $(opam env)
 
+echo "Running Z3 and bitwuzla ..."
 #### array-examples ####
-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
+python3 run_benchmarks.py --single --dir $ARRAY_EXAMPLES_DIR \
+  --output-dir csvs_single \
+  --output-filename array_examples_z3_solver \
+  --prover z3
+python3 run_benchmarks.py --single --dir $ARRAY_EXAMPLES_DIR \
+  --output-dir csvs_single \
+  --output-filename array_examples_z3 \
+  --prover smtml-z3
+python3 run_benchmarks.py --multi -F $ARRAY_EXAMPLES_LIST \
+  --output-dir csvs_multi \
+  --output-filename array_examples_z3 \
+  --prover smtml-z3
 
 #### array-industry-pattern ####
-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
+python3 run_benchmarks.py --single --dir $ARRAY_INDUSTRY_DIR \
+  --output-dir csvs_single \
+  --output-filename array_industry_pattern_z3_solver \
+  --prover z3
+python3 run_benchmarks.py --single --dir $ARRAY_INDUSTRY_DIR \
+  --output-dir csvs_single \
+  --output-filename array_industry_pattern_z3 \
+  --prover smtml-z3
+python3 run_benchmarks.py --multi -F $ARRAY_INDUSTRY_LIST \
+  --output-dir csvs_multi \
+  --output-filename array_industry_pattern_z3 \
+  --prover smtml-z3
 
 #### eca-rers2018 ####
-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
+python3 run_benchmarks.py --single --dir $ECA_DIR \
+  --output-dir csvs_single \
+  --output-filename eca_rers2018_z3_solver \
+  --prover z3
+python3 run_benchmarks.py --single --dir $ECA_DIR \
+  --output-dir csvs_single \
+  --output-filename eca_rers2018_z3 \
+  --prover smtml-z3
+python3 run_benchmarks.py --multi -F $ECA_LIST \
+  --output-dir csvs_multi \
+  --output-filename eca_rers2018_z3 \
+  --prover smtml-z3
 
 ## Plots ##
-python3 plots.py --testcomp --array-examples --output plot_array_examples_multi --files csvs_multi/array_examples_z3.csv csvs_single/array_examples_z3_solver.csv csvs_single/array_examples_z3.csv
-python3 plots.py --testcomp --array-industry-pattern --output plot_array_industry_pattern_multi --files csvs_multi/array_industry_pattern_z3.csv csvs_single/array_industry_pattern_z3_solver.csv csvs_single/array_industry_pattern_z3.csv
-python3 plots.py --testcomp --eca-rers2018 --output plot_eca_rers2018_multi --files csvs_multi/eca_rers2018_z3.csv csvs_single/eca_rers2018_z3_solver.csv csvs_single/eca_rers2018_z3.csv
\ No newline at end of file
+echo "Generating plots ..."
+python3 plots.py --testcomp --array-examples \
+  --output plot_array_examples_multi \
+  --files \
+  csvs_multi/array_examples_z3.csv \
+  csvs_single/array_examples_z3_solver.csv \
+  csvs_single/array_examples_z3.csv
+
+python3 plots.py --testcomp --array-industry-pattern \
+  --output plot_array_industry_pattern_multi \
+  --files \
+  csvs_multi/array_industry_pattern_z3.csv \
+  csvs_single/array_industry_pattern_z3_solver.csv \
+  csvs_single/array_industry_pattern_z3.csv
+
+python3 plots.py --testcomp --eca-rers2018 \
+  --output plot_eca_rers2018_multi \
+  --files \
+  csvs_multi/eca_rers2018_z3.csv \
+  csvs_single/eca_rers2018_z3_solver.csv \
+  csvs_single/eca_rers2018_z3.csv