diff --git a/scripts/benchmark/README.md b/scripts/benchmark/README.md
index e457d62928e..62fa8be1e1b 100644
--- a/scripts/benchmark/README.md
+++ b/scripts/benchmark/README.md
@@ -14,7 +14,7 @@ Assuming there is a java maven module installed in `project-name/module-core/`,
 and the `jbmc` main directory is in `/path/to/jbmc`, go to
 `project-name/module-core/target/classes`, and run:
 
-    /path/to/scripts/benchmark/benchmark_java_project.js /path/to/jbmc -l method_list_example.txt -a java_arguments.json -m path/to/jbmc/lib/java-models-library/target/core-models.jar | tee result.json
+    /path/to/scripts/benchmark/benchmark_java_project.js /path/to/jbmc -l method_list_example.txt -a jbmc_arguments_example.json -m path/to/jbmc/lib/java-models-library/target/core-models.jar | tee result.json
 
 This will display the results and save them into the file `result.json`.
 
@@ -29,9 +29,9 @@ This will create a `result.csv` file containing the results.
 # Comparing two runs
 
 Assuming the results have been converted to csv and saved into two files named
-benchmark1.csv and benchmark2.csv:
+develop.csv and branch.csv:
 
      gnuplot draw_scatter.gp
 
-will create a png file `perf_out.png` with the time from the first run on the
-`y` axis and the second on the `x` axis.
+will create a png file `perf_out.png` with the time from the branch / changed run on the
+`y` axis and the develop / original run on the `x` axis.
diff --git a/scripts/benchmark/benchmark_java_project.js b/scripts/benchmark/benchmark_java_project.js
index f57c67bba5a..4585597c371 100755
--- a/scripts/benchmark/benchmark_java_project.js
+++ b/scripts/benchmark/benchmark_java_project.js
@@ -66,7 +66,7 @@ function readNumberOfGoals(stdout) {
     return 0;
 }
 function readJsonFile(fileName) {
-    return JSON.parse(fs.readFileSync(filename, 'utf8'));
+    return JSON.parse(fs.readFileSync(fileName, 'utf8'));
 }
 
 /// Read the options from tools.json and launch the executable
@@ -92,7 +92,7 @@ function run(executable, modelsPath, argumentsFile, functionName,
     // timeout isn't a jbmc option but only used by this script
     const timeout = config.timeout;
     config['timeout'] = false;
-    commandLine = `${executable} ${classFile} ${configToString(config)}`
+    commandLine = `${executable} ${classFile} ${argsToString(config)}`
     const startTime = new Date();
     try {
         const timeCommand = "export TIME=\"%U\"; /usr/bin/time --quiet -o tmp_time.out "
diff --git a/scripts/benchmark/draw_scatter.gp b/scripts/benchmark/draw_scatter.gp
index 95c750a2736..1f1972ff7a8 100644
--- a/scripts/benchmark/draw_scatter.gp
+++ b/scripts/benchmark/draw_scatter.gp
@@ -7,8 +7,8 @@ set xrange [30:60000]
 set yrange [30:60000]
 set logscale x 10
 set logscale y 10
-set ylabel 'time (sec.) on branch'
 set xlabel 'time (sec.) on develop'
+set ylabel 'time (sec.) on branch'
 
-plot '< join benchmark1.csv benchmark2.csv' using 6:3 with points, \
+plot '< join develop.csv branch.csv' using 3:6 with points, \
   x with lines
diff --git a/scripts/benchmark/jbmc_arguments.json b/scripts/benchmark/jbmc_arguments_example.json
similarity index 100%
rename from scripts/benchmark/jbmc_arguments.json
rename to scripts/benchmark/jbmc_arguments_example.json