Artifact fixes

bench/README.md

@@ -10,7 +10,7 @@ solver usage, with notable improvements for batched solver interactions.
 
 ## Getting the Artifact
 
-You can download the artifact through [Zenodo](https://zenodo.org/records/13959671/files/smtml_0.3.tar.gz?download=1).
+You can download the artifact through [Zenodo](https://zenodo.org/records/14104822).
 
 ## Tested platforms
 
@@ -29,7 +29,7 @@ modification, and distribution.
 
 ## MD5 Hash of the Artifact
 
-8edce799971395168bdf728c9a136399
+46c6e43adf9bd5d9a922b3b7db307d12
 
 ## Building and Running the Docker Image
 
@@ -191,10 +191,14 @@ $ git submodule update --remote -- smt-comp/
 ```
 
 2. Run the `eq1.sh` script. Note that, this script can take up multiple
-hours to complete.
+hours to complete. Therefore, to avoid running the entire dataset specify
+a number of benchmark to run with the `-n` flag. This will run the benchmarks
+quicker, but only provide an aproximation of the papers results.
 
 ```sh
 $ ./eq1.sh
+# Or, to just run 20 benchmarks to finish quickly
+$ ./eq1.sh -n 20
 ```
 
 The script will generate the results in directory `eq1`, which
@@ -237,10 +241,14 @@ $ git submodule update --remote -- smt-comp/
 ```
 
 2. Run the `eq2.sh` script. Note that, this script can take up multiple
-hours to complete.
+hours to complete. Therefore, to avoid running the entire dataset specify
+a number of benchmark to run with the `-n` flag. This will run the benchmarks
+quicker, but only provide an aproximation of the papers results.
 
 ```sh
 $ ./eq2.sh
+# Or, to just run 20 benchmarks to finish quickly
+$ ./eq2.sh -n 20
 ```
 
 The script will generate the following files:
@@ -315,10 +323,14 @@ $ git submodule update --remote -- smt-testcomp23/
 ```
 
 2. Run the `testcomp.sh` script. Note that, this script can take up multiple
-hours to complete.
+hours to complete. Therefore, to avoid running the entire dataset specify
+a number of benchmark to run with the `-n` flag. This will run the benchmarks
+quicker, but only provide an aproximation of the papers results.
 
 ```sh
 $ ./testcomp.sh
+# Or, to just run 20 benchmarks to finish quickly
+$ ./testcomp.sh -n 20
 ```
 
 The script will generate the following files:

bench/eq1.sh

@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
 TEMPLATE=./tmp.XXXXXXXXXX
 

bench/eq2.sh

@@ -100,7 +100,7 @@ python3 run_benchmarks.py --single --dir $QF_LIA_DIR --output-dir csvs_single --
 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
+python3 run_benchmarks.py --single --dir $QF_BV_DIR --output-dir csvs_single --output-filename QF_BV_bitwuzla_solver --prover bitwuzla
 #### QF_S ####
 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

bench/eq3.sh

@@ -127,6 +127,8 @@ fi
 
 $dry_value && exit 0
 
+mkdir csvs_multi
+
 opam sw z3-bitwuzla
 eval $(opam env)
 
@@ -147,7 +149,7 @@ else
   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_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 --prover smtml-bitwuzla
 
 #### QF_LIA ####
 ## Z3 ##
@@ -176,7 +178,7 @@ else
   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_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 --prover smtml-bitwuzla
 
 #### QF_S ####
 ## Z3 ##

bench/run_benchmarks.py

@@ -32,7 +32,7 @@ def get_latest_sqlite_file(benchpress_data_dir):
   files = [f for f in os.listdir(benchpress_data_dir) if f.endswith('.sqlite')]
   if not files:
     raise FileNotFoundError("No .sqlite files found in benchpress data directory.")
-  
+
   latest_file = max(files, key=lambda x: os.path.getmtime(os.path.join(benchpress_data_dir, x)))
   return os.path.join(benchpress_data_dir, latest_file)
 
@@ -65,13 +65,13 @@ def automate_benchpress_single(directory_to_benchmark, output_csv_dir, output_cs
       print_error(f"Error during SQLite to CSV process: {e}")
 
 def get_latest_n_csvs(n):
-  result = subprocess.run(['ls', '-d', os.path.join('/home/smtml/smtml/bench', 'res-multi-query-*')], 
+  result = subprocess.run(['ls', '-d', os.path.join('/home/smtml/smtml/bench', 'res-multi-query-*')],
                             stdout=subprocess.PIPE, text=True, shell=True)
   query_dirs = result.stdout.splitlines()
   query_dirs = query_dirs[-n:]
   csv_files = []
   for query_dir in query_dirs:
-        csv_file = glob(os.path.join(query_dir, '*.csv'))
+        csv_file = glob.glob(os.path.join(query_dir, '*.csv'))
         if csv_file:
             csv_files.append(csv_file[0])
   return csv_files
@@ -135,4 +135,4 @@ def automate_multi_query(list_file, output_csv_dir, output_csv_name, prover):
   elif args.multi:
     automate_multi_query(args.F, args.output_dir, args.output_filename, args.prover)
   else:
-    print_error("Please specify --single or --multi.")
+    print_error("Please specify --single or --multi.")

bench/runner/multi_query.ml

@@ -75,11 +75,11 @@ let main _hook provers from_file dirs =
   let results =
     List.map
       (fun p ->
-        let ((status, stdout, _stderr, _) as result) =
+        let ((status, stdout, stderr, _) as result) =
           Tool.fork_and_run ?from_file p dirs
         in
-        Fmt.pr "@[<v 2>Run %a@;Exited: %a@;Stdout:@; %a@]@." Tool.pp_prover p
-          pp_exit_status status Fmt.string (String.escaped stdout);
+        Fmt.pr "@[<v 2>Run %a@;Exited: %a@;Stdout:@; %a@;Stderr:@; %a@]@." Tool.pp_prover p
+          pp_exit_status status Fmt.string (String.escaped stdout) Fmt.string (String.escaped stderr);
         (p, result) )
       provers
   in