From e89730c83a978739fb447b80103eb4b66e477a38 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sat, 24 Oct 2020 21:04:06 +0200
Subject: [PATCH 01/46] added a function to util to get data model from task

---
 benchexec/util.py | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/benchexec/util.py b/benchexec/util.py
index b2bd8f702..3a6efa076 100644
--- a/benchexec/util.py
+++ b/benchexec/util.py
@@ -762,3 +762,21 @@ def check_msr():
         if all(os.access("/dev/cpu/{}/msr".format(cpu), os.W_OK) for cpu in cpu_dirs):
             res["write"] = True
     return res
+
+
+def get_data_model_from_task(task, data_models):
+    # Importing it here, otherwise it will result in cyclic dependency.
+    import benchexec.tools.template
+    if isinstance(task.options, dict) and task.options.get("language") == "C":
+        data_model = task.options.get("data_model")
+        if data_model:
+            data_model_option = data_models.get(data_model)
+            if data_model_option:
+                return data_model_option
+            else:
+                raise benchexec.tools.template.UnsupportedFeatureException(
+                    "Unsupported data_model '{}' defined for task '{}'".format(
+                        data_model, task
+                    )
+                )
+    return None

From e9ecbf61b5c5b3b633a91650df3c620f819f1a8f Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sat, 24 Oct 2020 21:04:40 +0200
Subject: [PATCH 02/46] updated TI for 2ls

---
 benchexec/tools/two_ls.py | 30 +++++++++++++++++++-----------
 1 file changed, 19 insertions(+), 11 deletions(-)

diff --git a/benchexec/tools/two_ls.py b/benchexec/tools/two_ls.py
index fef2230da..08bfe2e6f 100644
--- a/benchexec/tools/two_ls.py
+++ b/benchexec/tools/two_ls.py
@@ -10,15 +10,15 @@
 import benchexec.result as result
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Wrapper for 2LS (http://www.cprover.org/2LS).
     """
 
     REQUIRED_PATHS = ["2ls", "2ls-binary", "goto-cc"]
 
-    def executable(self):
-        return util.find_executable("2ls")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("2ls")
 
     def name(self):
         return "2LS"
@@ -26,14 +26,22 @@ def name(self):
     def version(self, executable):
         return self._version_from_tool(executable)
 
-    def cmdline(self, executable, options, tasks, propertyfile, rlimits):
-        if propertyfile:
-            options = options + ["--propertyfile", propertyfile]
+    def cmdline(self, executable, options, task, rlimits):
+        if task.property_file:
+            options = options + ["--propertyfile", task.property_file]
 
-        return [executable] + options + tasks
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "--32", "LP64": "--64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
-        if ((returnsignal == 9) or (returnsignal == 15)) and isTimeout:
+        return [executable] + options + list(task.input_files_or_identifier)
+
+    def determine_result(self, run):
+        returnsignal = run.exit_code.signal or 0
+        returncode = run.exit_code.value or 0
+        if ((returnsignal == 9) or (returnsignal == 15)) and run.was_timeout:
             status = "TIMEOUT"
         elif returnsignal == 9:
             status = "OUT OF MEMORY"
@@ -42,8 +50,8 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
         elif returncode == 0:
             status = result.RESULT_TRUE_PROP
         elif returncode == 10:
-            if len(output) > 0:
-                result_str = output[-1].strip()
+            if len(run.output) > 0:
+                result_str = run.output[-1].strip()
                 if result_str == "FALSE(valid-memtrack)":
                     status = result.RESULT_FALSE_MEMTRACK
                 elif result_str == "FALSE(valid-deref)":

From a338d0526b8a6c71681a941611072f871d7518a7 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 12:10:04 +0100
Subject: [PATCH 03/46] updated TI for brick

---
 benchexec/tools/brick.py | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/benchexec/tools/brick.py b/benchexec/tools/brick.py
index b6870d48b..0103f563c 100644
--- a/benchexec/tools/brick.py
+++ b/benchexec/tools/brick.py
@@ -10,7 +10,7 @@
 import benchexec.result as result
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for BRICK
     https://github.com/brick-tool-dev/brick-tool
@@ -18,14 +18,20 @@ class Tool(benchexec.tools.template.BaseTool):
 
     REQUIRED_PATHS = ["bin", "lib"]
 
-    def executable(self):
-        return util.find_executable("bin/brick")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("brick", subdir="bin")
 
     def name(self):
         return "BRICK"
 
-    def cmdline(self, executable, options, tasks, propertyfile, rlimits):
-        return [executable] + options + tasks
+    def cmdline(self, executable, options, task, rlimits):
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "--32", "LP64": "--64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
+
+        return [executable] + options + list(task.input_files_or_identifier)
 
     def version(self, executable):
         return self._version_from_tool(executable, arg="--version")
@@ -36,10 +42,10 @@ def program_files(self, executable):
             executable, paths, parent_dir=True
         )
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
         status = result.RESULT_ERROR
 
-        for line in output:
+        for line in run.output._lines:
             if line == "VERIFICATION SUCCESSFUL\n":
                 status = result.RESULT_TRUE_PROP
                 break

From 171ec3e672fef901f2985c09d7ee82cf917b8261 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 12:26:00 +0100
Subject: [PATCH 04/46] updated TI for cbmc

---
 benchexec/tools/cbmc.py | 27 ++++++++++++++++++---------
 1 file changed, 18 insertions(+), 9 deletions(-)

diff --git a/benchexec/tools/cbmc.py b/benchexec/tools/cbmc.py
index b9c5eb3ac..dc14a17ef 100644
--- a/benchexec/tools/cbmc.py
+++ b/benchexec/tools/cbmc.py
@@ -13,7 +13,7 @@
 import benchexec.result as result
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for CBMC (http://www.cprover.org/cbmc/).
     It always adds --xml-ui to the command-line arguments for easier parsing of
@@ -23,8 +23,8 @@ class Tool(benchexec.tools.template.BaseTool):
 
     REQUIRED_PATHS = ["cbmc", "cbmc-binary", "goto-cc"]
 
-    def executable(self):
-        return util.find_executable("cbmc")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("cbmc")
 
     def version(self, executable):
         return self._version_from_tool(executable)
@@ -32,15 +32,21 @@ def version(self, executable):
     def name(self):
         return "CBMC"
 
-    def cmdline(self, executable, options, tasks, propertyfile, rlimits):
-        if propertyfile:
-            options = options + ["--propertyfile", propertyfile]
+    def cmdline(self, executable, options, task, rlimits):
+        if task.property_file:
+            options = options + ["--propertyfile", task.property_file]
         elif "--xml-ui" not in options:
             options = options + ["--xml-ui"]
 
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "--32", "LP64": "--64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
+
         self.options = options
 
-        return [executable] + options + tasks
+        return [executable] + options + list(task.input_files_or_identifier)
 
     def parse_XML(self, output, returncode, isTimeout):
         # an empty tag cannot be parsed into a tree
@@ -102,12 +108,15 @@ def isErrorMessage(msg):
 
         return status
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
+        returnsignal = run.exit_code.signal or 0
+        returncode = run.exit_code.value or 0
+        output = run.output
 
         if returnsignal == 0 and ((returncode == 0) or (returncode == 10)):
             status = result.RESULT_ERROR
             if "--xml-ui" in self.options:
-                status = self.parse_XML(output, returncode, isTimeout)
+                status = self.parse_XML(output, returncode, run.was_timeout)
             elif len(output) > 0:
                 # SV-COMP mode
                 result_str = output[-1].strip()

From ac4546bc5774699ca2fb43c422d9aa0ae9f15667 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 12:48:01 +0100
Subject: [PATCH 05/46] updated TI for divine

---
 benchexec/tools/divine.py  | 30 ++++++++++++++++++++----------
 benchexec/tools/divine4.py | 30 +++++++++++++++++++-----------
 2 files changed, 39 insertions(+), 21 deletions(-)

diff --git a/benchexec/tools/divine.py b/benchexec/tools/divine.py
index 2ae674629..99ee5b8f4 100644
--- a/benchexec/tools/divine.py
+++ b/benchexec/tools/divine.py
@@ -12,7 +12,7 @@
 import os
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     DIVINE info object
     """
@@ -33,14 +33,14 @@ class Tool(benchexec.tools.template.BaseTool):
         "libz.so.1",
     ]
 
-    def executable(self):
+    def executable(self, tool_locator):
         """
         Find the path to the executable file that will get executed.
         This method always needs to be overridden,
         and most implementations will look similar to this one.
         The path returned should be relative to the current directory.
         """
-        return util.find_executable(self.BINS[0], os.path.join("bin", self.BINS[0]))
+        return tool_locator.find_executable(self.BINS[0], subdir="bin")
 
     def version(self, executable):
         return self._version_from_tool(executable)
@@ -51,7 +51,7 @@ def name(self):
         """
         return "DIVINE"
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
+    def cmdline(self, executable, options, task, rlimits):
         """
         Compose the command line to execute from the name of the executable,
         the user-specified options, and the inputfile to analyze.
@@ -70,13 +70,23 @@ def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
                         for example: time-limit, soft-time-limit, hard-time-limit, memory-limit, cpu-core-limit.
                         All entries in rlimits are optional, so check for existence before usage!
         """
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "--32", "LP64": "--64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
+
         directory = os.path.dirname(executable)
 
         # Ignore propertyfile since we run only reachability
-        run = [os.path.join(".", directory, self.BINS[1]), directory] + options + tasks
+        run = (
+            [os.path.join(".", directory, self.BINS[1]), directory]
+            + options
+            + list(task.input_files_or_identifier)
+        )
         return run
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
         """
         Parse the output of the tool and extract the verification result.
         This method always needs to be overridden.
@@ -87,15 +97,15 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
         """
 
-        if not output:
+        if not run.output:
             return "ERROR - no output"
 
-        last = output[-1]
+        last = run.output[-1]
 
-        if isTimeout:
+        if run.was_timeout:
             return "TIMEOUT"
 
-        if returncode != 0:
+        if run.exit_code.value != 0:
             return "ERROR - Pre-run"
 
         if last is None:
diff --git a/benchexec/tools/divine4.py b/benchexec/tools/divine4.py
index d810b9cfc..743721eed 100644
--- a/benchexec/tools/divine4.py
+++ b/benchexec/tools/divine4.py
@@ -13,7 +13,7 @@
 import os
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     DIVINE tool info object
     """
@@ -31,12 +31,12 @@ class Tool(benchexec.tools.template.BaseTool):
         "false-overflow": result.RESULT_FALSE_OVERFLOW,
     }
 
-    def executable(self):
+    def executable(self, tool_locator):
         """
         Find the path to the executable file that will get executed.
         The path returned should be relative to the current directory.
         """
-        return util.find_executable(self.BINS[0])
+        return tool_locator.find_executable(self.BINS[0])
 
     def version(self, executable):
         return self._version_from_tool(
@@ -49,7 +49,7 @@ def name(self):
         """
         return "DIVINE"
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
+    def cmdline(self, executable, options, task, rlimits):
         """
         Compose the command line to execute from the name of the executable,
         the user-specified options, and the inputfile to analyze.
@@ -68,15 +68,23 @@ def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
                         for example: time-limit, soft-time-limit, hard-time-limit, memory-limit, cpu-core-limit.
                         All entries in rlimits are optional, so check for existence before usage!
         """
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "--32", "LP64": "--64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
+
         directory = os.path.dirname(executable)
-        prp = propertyfile or "-"
+        prp = task.property_file or "-"
 
         # prefix command line with wrapper script
         return (
-            [os.path.join(directory, self.BINS[1]), executable, prp] + options + tasks
+            [os.path.join(directory, self.BINS[1]), executable, prp]
+            + options
+            + list(task.input_files_or_identifier)
         )
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
         """
         Parse the output of the tool and extract the verification result.
         This method always needs to be overridden.
@@ -87,15 +95,15 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
         """
 
-        if not output:
+        if not run.output:
             return "ERROR - no output"
 
-        last = output[-1]
+        last = run.output[-1]
 
-        if isTimeout:
+        if run.was_timeout:
             return "TIMEOUT"
 
-        if returncode != 0:
+        if run.exit_code.value != 0:
             return "ERROR - {0}".format(last)
 
         if "result:" in last:

From 5699042def7a1526cbbf963c7482c4bbda618dd0 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 13:23:18 +0100
Subject: [PATCH 06/46] updated TI for esbmc

---
 benchexec/tools/esbmc.py | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

diff --git a/benchexec/tools/esbmc.py b/benchexec/tools/esbmc.py
index 636eedcee..3523c93b9 100644
--- a/benchexec/tools/esbmc.py
+++ b/benchexec/tools/esbmc.py
@@ -11,15 +11,15 @@
 import benchexec.result as result
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     This class serves as tool adaptor for ESBMC (http://www.esbmc.org/)
     """
 
     REQUIRED_PATHS = ["cpachecker", "esbmc", "esbmc-wrapper.py", "tokenizer"]
 
-    def executable(self):
-        return util.find_executable("esbmc-wrapper.py")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("esbmc-wrapper.py")
 
     def working_directory(self, executable):
         executableDir = os.path.dirname(executable)
@@ -31,13 +31,20 @@ def version(self, executable):
     def name(self):
         return "ESBMC"
 
-    def cmdline(self, executable, options, tasks, propertyfile, rlimits):
+    def cmdline(self, executable, options, task, rlimits):
+        tasks = list(task.input_files_or_identifier)
         assert len(tasks) == 1, "only one inputfile supported"
         inputfile = tasks[0]
-        return [executable] + ["-p", propertyfile] + options + [inputfile]
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
-        output = "\n".join(output)
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "32", "LP64": "64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += ["--arch", data_model_param]
+        return [executable] + ["-p", task.property_file] + options + [inputfile]
+
+    def determine_result(self, run):
+        output = "\n".join(run.output)
         status = result.RESULT_UNKNOWN
 
         if self.allInText(["FALSE_DEREF"], output):
@@ -58,7 +65,7 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
             status = result.RESULT_DONE
 
         if status == result.RESULT_UNKNOWN:
-            if isTimeout:
+            if run.was_timeout:
                 status = "TIMEOUT"
             elif output.endswith(("error", "error\n")):
                 status = "ERROR"

From 904cc513c4db76b14a77092ed43932e3462634a1 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 13:44:42 +0100
Subject: [PATCH 07/46] updated TI for gacal

---
 benchexec/tools/gacal.py | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/benchexec/tools/gacal.py b/benchexec/tools/gacal.py
index 73c023113..3c96cbaef 100644
--- a/benchexec/tools/gacal.py
+++ b/benchexec/tools/gacal.py
@@ -10,7 +10,7 @@
 import benchexec.result as result
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for GACAL.
     URL: https://gitlab.com/bquiring/sv-comp-submission
@@ -25,8 +25,8 @@ class Tool(benchexec.tools.template.BaseTool):
         "scripts",
     ]
 
-    def executable(self):
-        return util.find_executable("run-gacal.py")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("run-gacal.py")
 
     def name(self):
         return "GACAL"
@@ -34,11 +34,17 @@ def name(self):
     def version(self, executable):
         return self._version_from_tool(executable)
 
-    def cmdline(self, executable, options, tasks, propertyfile, rlimits):
-        return [executable] + options + tasks
+    def cmdline(self, executable, options, task, rlimits):
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "32", "LP64": "64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += ["--architecture", data_model_param]
 
-    def determine_result(self, returncode, returnsignal, output, is_timeout):
-        for line in output:
+        return [executable] + options + list(task.input_files_or_identifier)
+
+    def determine_result(self, run):
+        for line in run.output:
             if "VERIFICATION_SUCCESSFUL" in line:
                 return result.RESULT_TRUE_PROP
             elif "VERIFICATION_FAILED" in line:

From fccc1b68e2c004660498bfaa0f18e570bcdf7b86 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 13:57:46 +0100
Subject: [PATCH 08/46] updated TI for cseq based tools

---
 benchexec/tools/cseq.py          | 11 ++++++-----
 benchexec/tools/lazycseq.py      |  5 ++---
 benchexec/tools/lazycseqabs.py   |  5 ++---
 benchexec/tools/lazycseqswarm.py |  5 ++---
 4 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/benchexec/tools/cseq.py b/benchexec/tools/cseq.py
index 2add04e65..587367b09 100644
--- a/benchexec/tools/cseq.py
+++ b/benchexec/tools/cseq.py
@@ -9,7 +9,7 @@
 import benchexec.result as result
 
 
-class CSeqTool(benchexec.tools.template.BaseTool):
+class CSeqTool(benchexec.tools.template.BaseTool2):
     """
     Abstract tool info for CSeq-based tools (http://users.ecs.soton.ac.uk/gp4/cseq/cseq.html).
     """
@@ -19,7 +19,7 @@ def version(self, executable):
         first_line = output.splitlines()[0]
         return first_line.strip()
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
+    def cmdline(self, executable, options, task, rlimits):
         """
         Compose the command line to execute from the name of the executable,
         the user-specified options, and the inputfile to analyze.
@@ -36,13 +36,14 @@ def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
                         for example: time-limit, soft-time-limit, hard-time-limit, memory-limit, cpu-core-limit.
                         All entries in rlimits are optional, so check for existence before usage!
         """
+        tasks = list(task.input_files_or_identifier)
         assert len(tasks) == 1, "only one inputfile supported"
         inputfile = ["--input", tasks[0]]
-        spec = ["--spec", propertyfile] if propertyfile is not None else []
+        spec = ["--spec", task.property_file] if task.property_file is not None else []
         return [executable] + options + spec + inputfile
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
-        output = "\n".join(output)
+    def determine_result(self, run):
+        output = "\n".join(run.output)
         status = result.RESULT_UNKNOWN
         if "FALSE" in output:
             status = result.RESULT_FALSE_REACH
diff --git a/benchexec/tools/lazycseq.py b/benchexec/tools/lazycseq.py
index e62ace62f..b08b430a2 100644
--- a/benchexec/tools/lazycseq.py
+++ b/benchexec/tools/lazycseq.py
@@ -5,7 +5,6 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
 from . import cseq
 
 
@@ -27,8 +26,8 @@ class Tool(cseq.CSeqTool):
         "backends",
     ]
 
-    def executable(self):
-        return util.find_executable("lazy-cseq.py")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("lazy-cseq.py")
 
     def name(self):
         return "Lazy-CSeq"
diff --git a/benchexec/tools/lazycseqabs.py b/benchexec/tools/lazycseqabs.py
index b88f75af6..eb4aa8c3c 100644
--- a/benchexec/tools/lazycseqabs.py
+++ b/benchexec/tools/lazycseqabs.py
@@ -5,7 +5,6 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
 from . import cseq
 
 
@@ -23,8 +22,8 @@ class Tool(cseq.CSeqTool):
         "modules",
     ]
 
-    def executable(self):
-        return util.find_executable("lazy-cseq-abs.py")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("lazy-cseq-abs.py")
 
     def name(self):
         return "Lazy-CSeq-Abs"
diff --git a/benchexec/tools/lazycseqswarm.py b/benchexec/tools/lazycseqswarm.py
index bcc4ab4d8..deb7e14fb 100644
--- a/benchexec/tools/lazycseqswarm.py
+++ b/benchexec/tools/lazycseqswarm.py
@@ -5,7 +5,6 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
 from . import cseq
 
 
@@ -24,8 +23,8 @@ class Tool(cseq.CSeqTool):
         "modules",
     ]
 
-    def executable(self):
-        return util.find_executable("lazy-cseq-swarm.py")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("lazy-cseq-swarm.py")
 
     def name(self):
         return "Lazy-CSeq-Swarm"

From 7de8b86a3ecfcca09573c3ace374d49ff2fcf9e2 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 14:11:52 +0100
Subject: [PATCH 09/46] updated TI for pinaka

---
 benchexec/tools/pinaka.py | 28 ++++++++++++++++++----------
 1 file changed, 18 insertions(+), 10 deletions(-)

diff --git a/benchexec/tools/pinaka.py b/benchexec/tools/pinaka.py
index 18b318350..720dde045 100644
--- a/benchexec/tools/pinaka.py
+++ b/benchexec/tools/pinaka.py
@@ -10,12 +10,12 @@
 import benchexec.result as result
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
 
     REQUIRED_PATHS = ["pinaka-wrapper.sh", "pinaka"]
 
-    def executable(self):
-        return util.find_executable("pinaka-wrapper.sh")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("pinaka-wrapper.sh")
 
     def version(self, executable):
         return self._version_from_tool(executable)
@@ -23,13 +23,21 @@ def version(self, executable):
     def name(self):
         return "Pinaka"
 
-    def cmdline(self, executable, options, tasks, propertyfile, rlimits):
-        if propertyfile:
-            options = options + ["--propertyfile", propertyfile]
-
-        return [executable] + options + tasks
-
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def cmdline(self, executable, options, task, rlimits):
+        if task.property_file:
+            options = options + ["--propertyfile", task.property_file]
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "--32", "LP64": "--64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
+
+        return [executable] + options + list(task.input_files_or_identifier)
+
+    def determine_result(self, run):
+        returnsignal = run.exit_code.signal or 0
+        returncode = run.exit_code.value or 0
+        output = run.output._lines
         status = ""
 
         if returnsignal == 0 and ((returncode == 0) or (returncode == 10)):

From eeaf036effbfe829c4645bd211ca0412cfa0b45a Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 14:20:51 +0100
Subject: [PATCH 10/46] updated TI for predatorHP

---
 benchexec/tools/predatorhp.py | 29 ++++++++++++++++++++---------
 1 file changed, 20 insertions(+), 9 deletions(-)

diff --git a/benchexec/tools/predatorhp.py b/benchexec/tools/predatorhp.py
index 364b702bb..72157862b 100644
--- a/benchexec/tools/predatorhp.py
+++ b/benchexec/tools/predatorhp.py
@@ -10,7 +10,7 @@
 import benchexec.result as result
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Wrapper for a Predator - Hunting Party
     http://www.fit.vutbr.cz/research/groups/verifit/tools/predator-hp/
@@ -18,8 +18,8 @@ class Tool(benchexec.tools.template.BaseTool):
 
     REQUIRED_PATHS = ["predator", "predator-bfs", "predator-dfs", "predatorHP.py"]
 
-    def executable(self):
-        return util.find_executable("predatorHP.py")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("predatorHP.py")
 
     def name(self):
         return "PredatorHP"
@@ -27,12 +27,23 @@ def name(self):
     def version(self, executable):
         return self._version_from_tool(executable, use_stderr=True)
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
-        spec = ["--propertyfile", propertyfile] if propertyfile is not None else []
-        return [executable] + options + spec + tasks
+    def cmdline(self, executable, options, task, rlimits):
+        spec = (
+            ["--propertyfile", task.property_file]
+            if task.property_file is not None
+            else []
+        )
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
-        output = "\n".join(output)
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "-m32", "LP64": "-m64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += ["--compiler-options", data_model_param]
+
+        return [executable] + options + spec + list(task.input_files_or_identifier)
+
+    def determine_result(self, run):
+        output = "\n".join(run.output)
         status = "UNKNOWN"
         if "UNKNOWN" in output:
             status = result.RESULT_UNKNOWN
@@ -48,6 +59,6 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
             status = result.RESULT_FALSE_MEMCLEANUP
         elif "FALSE" in output:
             status = result.RESULT_FALSE_REACH
-        if status == "UNKNOWN" and isTimeout:
+        if status == "UNKNOWN" and run.was_timeout:
             status = "TIMEOUT"
         return status

From 4760903236b322a894b7f9c6e53946e8dda6621c Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 14:45:45 +0100
Subject: [PATCH 11/46] updated TI for symbiotic

---
 benchexec/tools/symbiotic.py  | 43 +++++++++++++++++++----------------
 benchexec/tools/symbiotic4.py | 28 ++++++++++++++---------
 2 files changed, 41 insertions(+), 30 deletions(-)

diff --git a/benchexec/tools/symbiotic.py b/benchexec/tools/symbiotic.py
index 846cc808f..282cebaa6 100644
--- a/benchexec/tools/symbiotic.py
+++ b/benchexec/tools/symbiotic.py
@@ -6,8 +6,8 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
 import benchexec.result as result
+from benchexec.tools.template import ToolNotFoundException
 
 from .symbiotic4 import Tool as OldSymbiotic
 
@@ -25,19 +25,21 @@ class Tool(OldSymbiotic):
 
     REQUIRED_PATHS_7_0_0 = ["bin", "include", "properties", "lib", "llvm-8.0.1"]
 
-    def executable(self):
+    def executable(self, tool_locator):
         """
         Find the path to the executable file that will get executed.
         This method always needs to be overridden,
         and most implementations will look similar to this one.
         The path returned should be relative to the current directory.
         """
-        exe = util.find_executable("bin/symbiotic", exitOnError=False)
-        if exe:
-            return exe
-        else:
+        # This is used in the function _version_newer_than.
+        # I don't know a better way to do it.
+        self.tool_locator = tool_locator
+        try:
+            return tool_locator.find_executable("symbiotic", subdir="bin")
+        except ToolNotFoundException:
             # this may be the old version of Symbiotic
-            return OldSymbiotic.executable(self)
+            return OldSymbiotic.executable(self, tool_locator)
 
     def program_files(self, executable):
         if self._version_newer_than("7.0.0"):
@@ -59,7 +61,7 @@ def _version_newer_than(self, vers):
         """
         Determine whether the version is greater than some given version
         """
-        v = self.version(self.executable())
+        v = self.version(self.executable(self.tool_locator))
         vers_num = v[: v.index("-")]
         if not vers_num[0].isdigit():
             # this is the old version which is "older" than any given version
@@ -102,12 +104,15 @@ def _getPhase(self, output):
 
         return lastphase
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
-        if output is None:
+    def determine_result(self, run):
+        returnsignal = run.exit_code.signal or 0
+        returncode = run.exit_code.value or 0
+
+        if run.output is None:
             return "{0}(no output)".format(result.RESULT_ERROR)
 
         if self._version_newer_than("4.0.1"):
-            for line in output:
+            for line in run.output:
                 line = line.strip()
                 if line == "RESULT: true":
                     return result.RESULT_TRUE_PROP
@@ -131,19 +136,19 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
                     return result.RESULT_FALSE_REACH
         else:
             # old version of Symbiotic
-            return OldSymbiotic.determine_result(
-                self, returncode, returnsignal, output, isTimeout
-            )
+            return OldSymbiotic.determine_result(self, run)
 
-        if isTimeout:
-            return self._getPhase(output)  # generates TIMEOUT(phase)
+        if run.was_timeout:
+            return self._getPhase(run.output)  # generates TIMEOUT(phase)
         elif returnsignal != 0:
             return "KILLED (signal {0}, {1})".format(
-                returnsignal, self._getPhase(output)
+                returnsignal, self._getPhase(run.output)
             )
         elif returncode != 0:
             return "{0}(returned {1}, {2})".format(
-                result.RESULT_ERROR, returncode, self._getPhase(output)
+                result.RESULT_ERROR, returncode, self._getPhase(run.output)
             )
 
-        return "{0}(unknown, {1})".format(result.RESULT_ERROR, self._getPhase(output))
+        return "{0}(unknown, {1})".format(
+            result.RESULT_ERROR, self._getPhase(run.output)
+        )
diff --git a/benchexec/tools/symbiotic4.py b/benchexec/tools/symbiotic4.py
index cdfbc9db4..0492e0e8e 100644
--- a/benchexec/tools/symbiotic4.py
+++ b/benchexec/tools/symbiotic4.py
@@ -10,7 +10,7 @@
 import benchexec.result as result
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Symbiotic tool info object
     """
@@ -25,14 +25,14 @@ class Tool(benchexec.tools.template.BaseTool):
         "symbiotic",
     ]
 
-    def executable(self):
+    def executable(self, tool_locator):
         """
         Find the path to the executable file that will get executed.
         This method always needs to be overridden,
         and most implementations will look similar to this one.
         The path returned should be relative to the current directory.
         """
-        return util.find_executable("symbiotic")
+        return tool_locator.find_executable("symbiotic")
 
     def version(self, executable):
         """
@@ -46,24 +46,30 @@ def name(self):
         """
         return "symbiotic"
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
+    def cmdline(self, executable, options, task, rlimits):
         """
         Compose the command line to execute from the name of the executable
         """
 
-        if propertyfile is not None:
-            options = options + ["--prp={0}".format(propertyfile)]
+        if task.property_file is not None:
+            options = options + ["--prp={0}".format(task.property_file)]
 
-        return [executable] + options + tasks
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "--32", "LP64": "--64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
-        if isTimeout:
+        return [executable] + options + list(task.input_files_or_identifier)
+
+    def determine_result(self, run):
+        if run.was_timeout:
             return "timeout"
 
-        if output is None:
+        if run.output is None:
             return "error (no output)"
 
-        for line in output:
+        for line in run.output:
             line = line.strip()
             if line == "TRUE":
                 return result.RESULT_TRUE_PROP

From 3951a121d383740475edc497f87b8f81fc1af2ab Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 14:59:56 +0100
Subject: [PATCH 12/46] updated TI for verifuzz

---
 benchexec/tools/verifuzz.py | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/benchexec/tools/verifuzz.py b/benchexec/tools/verifuzz.py
index cdca07193..4e69f31d2 100644
--- a/benchexec/tools/verifuzz.py
+++ b/benchexec/tools/verifuzz.py
@@ -5,6 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
+import benchexec.util as util
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -43,6 +44,13 @@ def name(self):
     def cmdline(self, executable, options, task, rlimits):
         if task.property_file:
             options = options + ["--propertyFile", task.property_file]
+
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "32", "LP64": "64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += ["--bit", data_model_param]
+
         return [executable] + options + [task.single_input_file]
 
     def determine_result(self, run):

From e52a1385a92e0ce13c5cc8e05db75f1d6e66f616 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 20:30:05 +0100
Subject: [PATCH 13/46] applied black

---
 benchexec/util.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/benchexec/util.py b/benchexec/util.py
index 3a6efa076..6a42c2375 100644
--- a/benchexec/util.py
+++ b/benchexec/util.py
@@ -767,6 +767,7 @@ def check_msr():
 def get_data_model_from_task(task, data_models):
     # Importing it here, otherwise it will result in cyclic dependency.
     import benchexec.tools.template
+
     if isinstance(task.options, dict) and task.options.get("language") == "C":
         data_model = task.options.get("data_model")
         if data_model:

From 35c0703b0f16fe2cee3a7f10c24533eacd2feb21 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Sun, 25 Oct 2020 21:01:17 +0100
Subject: [PATCH 14/46] updated TI for fshell validator

---
 benchexec/tools/fshell-witness2test.py | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

diff --git a/benchexec/tools/fshell-witness2test.py b/benchexec/tools/fshell-witness2test.py
index a4808eac6..8f76ba270 100644
--- a/benchexec/tools/fshell-witness2test.py
+++ b/benchexec/tools/fshell-witness2test.py
@@ -12,7 +12,7 @@
 import benchexec.util as util
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for witness2test
     (https://github.com/diffblue/cprover-sv-comp/pull/14).
@@ -25,12 +25,12 @@ class Tool(benchexec.tools.template.BaseTool):
         "pycparser-master",
     ]
 
-    def executable(self):
+    def executable(self, tool_locator):
         """
         Find the path to the executable file that will get executed.
         @return a string pointing to an executable file
         """
-        return util.find_executable("test-gen.sh")
+        return tool_locator.find_executable("test-gen.sh")
 
     def version(self, executable):
         return self._version_from_tool(executable)
@@ -42,7 +42,7 @@ def name(self):
         """
         return "CProver witness2test"
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
+    def cmdline(self, executable, options, task, rlimits):
         """
         Compose the command line to execute from the name of the executable,
         the user-specified options, and the inputfile to analyze.
@@ -60,11 +60,18 @@ def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
                         All entries in rlimits are optional, so check for existence before usage!
         @return a list of strings that represent the command line to execute
         """
-        if propertyfile:
-            options = options + ["--propertyfile", propertyfile]
-        return [executable] + options + tasks
+        if task.property_file:
+            options = options + ["--propertyfile", task.property_file]
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+        data_model_param = util.get_data_model_from_task(
+            task, {"ILP32": "-m32", "LP64": "-m64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
+
+        return [executable] + options + list(task.input_files_or_identifier)
+
+    def determine_result(self, run):
         """
         Parse the output of the tool and extract the verification result.
         This method always needs to be overridden.
@@ -80,6 +87,9 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
         (useful to distinguish between program killed because of error and timeout)
         @return a non-empty string, usually one of the benchexec.result.RESULT_* constants
         """
+        returnsignal = run.exit_code.signal or 0
+        returncode = run.exit_code.value or 0
+        output = run.output
         status = result.RESULT_ERROR
         if returnsignal == 0 and returncode == 0:
             if output:

From 7a9da01fb548c5919484e30bb875b34db3770375 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Mon, 26 Oct 2020 08:13:50 +0100
Subject: [PATCH 15/46] updated TI for dartagnan

---
 benchexec/tools/dartagnan.py | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/benchexec/tools/dartagnan.py b/benchexec/tools/dartagnan.py
index 1e1e1099f..f2845e8d9 100644
--- a/benchexec/tools/dartagnan.py
+++ b/benchexec/tools/dartagnan.py
@@ -5,12 +5,11 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
 import benchexec.tools.template
 import benchexec.result as result
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for Dartagnan (https://github.com/hernanponcedeleon/Dat3M).
     """
@@ -24,22 +23,22 @@ class Tool(benchexec.tools.template.BaseTool):
         "output",
     ]
 
-    def executable(self):
-        return util.find_executable("./Dartagnan-SVCOMP.sh")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("Dartagnan-SVCOMP.sh")
 
     def name(self):
         return "Dartagnan"
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
-        return [executable] + options + tasks
+    def cmdline(self, executable, options, task, rlimits):
+        return [executable] + options + list(task.input_files_or_identifier)
 
     def version(self, executable):
         return self._version_from_tool(executable)
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
         status = result.RESULT_ERROR
-        if output:
-            result_str = output[-1].strip()
+        if run.output:
+            result_str = run.output[-1].strip()
             if "FAIL" in result_str:
                 status = result.RESULT_FALSE_REACH
             elif "PASS" in result_str:

From 0c3a85195199b7f794236743b052d205f335b597 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Mon, 26 Oct 2020 08:23:44 +0100
Subject: [PATCH 16/46] updated TI for map2check

---
 benchexec/tools/map2check.py | 37 +++++++++++++++++++++---------------
 1 file changed, 22 insertions(+), 15 deletions(-)

diff --git a/benchexec/tools/map2check.py b/benchexec/tools/map2check.py
index 6669c3957..683f33dd3 100644
--- a/benchexec/tools/map2check.py
+++ b/benchexec/tools/map2check.py
@@ -6,12 +6,12 @@
 # SPDX-License-Identifier: Apache-2.0
 
 import os
-import benchexec.util as util
 import benchexec.tools.template
 import benchexec.result as result
+from benchexec.tools.template import ToolNotFoundException
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     This class serves as tool adaptor for Map2Check (https://github.com/hbgit/Map2Check)
     """
@@ -25,12 +25,15 @@ class Tool(benchexec.tools.template.BaseTool):
 
     REQUIRED_PATHS_7_1 = ["map2check", "map2check-wrapper.py", "bin", "include", "lib"]
 
-    def executable(self):
+    def executable(self, tool_locator):
+        # This is used in _get_version
+        self._tool_locator = tool_locator
+
         # Relative path to map2check wrapper
         if self._get_version() == 6:
-            return util.find_executable("map2check-wrapper.sh")
+            return tool_locator.find_executable("map2check-wrapper.sh")
         elif self._get_version() > 6:
-            return util.find_executable("map2check-wrapper.py")
+            return tool_locator.find_executable("map2check-wrapper.py")
         assert False, "Unexpected version " + self._get_version()
 
     def program_files(self, executable):
@@ -48,10 +51,10 @@ def _get_version(self):
         """
         Determine the version based on map2check-wrapper.sh file
         """
-        exe_v6 = util.find_executable("map2check-wrapper.sh", exitOnError=False)
-        if exe_v6:
+        try:
+            self._tool_locator.find_executable("map2check-wrapper.sh")
             return 6
-        else:
+        except ToolNotFoundException:
             return 7
 
     def working_directory(self, executable):
@@ -64,17 +67,21 @@ def version(self, executable):
     def name(self):
         return "Map2Check"
 
-    def cmdline(self, executable, options, sourcefiles, propertyfile, rlimits):
+    def cmdline(self, executable, options, task, rlimits):
+        sourcefiles = list(task.input_files_or_identifier)
+
         assert len(sourcefiles) == 1, "only one sourcefile supported"
-        assert propertyfile, "property file required"
+        assert task.property_file, "property file required"
+
         sourcefile = sourcefiles[0]
         if self._get_version() == 6:
-            return [executable] + options + ["-c", propertyfile, sourcefile]
+            return [executable] + options + ["-c", task.property_file, sourcefile]
         elif self._get_version() > 6:
-            return [executable] + options + ["-p", propertyfile, sourcefile]
+            return [executable] + options + ["-p", task.property_file, sourcefile]
         assert False, "Unexpected version " + self._get_version()
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
+        output = run.output
         if not output:
             return result.RESULT_UNKNOWN
         output = output[-1].strip()
@@ -98,7 +105,7 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
                     status = result.RESULT_FALSE_REACH
             elif output.endswith("UNKNOWN"):
                 status = result.RESULT_UNKNOWN
-            elif isTimeout:
+            elif run.was_timeout:
                 status = "TIMEOUT"
             else:
                 status = "ERROR"
@@ -115,7 +122,7 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
                     status = result.RESULT_FALSE_FREE
             elif output.endswith("UNKNOWN"):
                 status = result.RESULT_UNKNOWN
-            elif isTimeout:
+            elif run.was_timeout:
                 status = "TIMEOUT"
             else:
                 status = "ERROR"

From fb5a18e4382326ea40bdaa4ebfb99b456f6a0ebb Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Mon, 26 Oct 2020 09:14:38 +0100
Subject: [PATCH 17/46] storing the version information beforehand for
 map2check and symbiotic

---
 benchexec/tools/map2check.py | 39 +++++++++++++-----------------------
 benchexec/tools/symbiotic.py | 13 ++++++------
 2 files changed, 20 insertions(+), 32 deletions(-)

diff --git a/benchexec/tools/map2check.py b/benchexec/tools/map2check.py
index 683f33dd3..e00137adf 100644
--- a/benchexec/tools/map2check.py
+++ b/benchexec/tools/map2check.py
@@ -26,37 +26,26 @@ class Tool(benchexec.tools.template.BaseTool2):
     REQUIRED_PATHS_7_1 = ["map2check", "map2check-wrapper.py", "bin", "include", "lib"]
 
     def executable(self, tool_locator):
-        # This is used in _get_version
-        self._tool_locator = tool_locator
+        try:
+            executable = tool_locator.find_executable("map2check-wrapper.sh")
+            self.__version = 6
+        except ToolNotFoundException:
+            executable = tool_locator.find_executable("map2check-wrapper.py")
+            self.__version = 7
 
-        # Relative path to map2check wrapper
-        if self._get_version() == 6:
-            return tool_locator.find_executable("map2check-wrapper.sh")
-        elif self._get_version() > 6:
-            return tool_locator.find_executable("map2check-wrapper.py")
-        assert False, "Unexpected version " + self._get_version()
+        return executable
 
     def program_files(self, executable):
         """
         Determine the file paths to be adopted
         """
-        if self._get_version() == 6:
+        if self.__version == 6:
             paths = self.REQUIRED_PATHS_6
-        elif self._get_version() > 6:
+        elif self.__version > 6:
             paths = self.REQUIRED_PATHS_7_1
 
         return paths
 
-    def _get_version(self):
-        """
-        Determine the version based on map2check-wrapper.sh file
-        """
-        try:
-            self._tool_locator.find_executable("map2check-wrapper.sh")
-            return 6
-        except ToolNotFoundException:
-            return 7
-
     def working_directory(self, executable):
         executableDir = os.path.dirname(executable)
         return executableDir
@@ -74,11 +63,11 @@ def cmdline(self, executable, options, task, rlimits):
         assert task.property_file, "property file required"
 
         sourcefile = sourcefiles[0]
-        if self._get_version() == 6:
+        if self.__version == 6:
             return [executable] + options + ["-c", task.property_file, sourcefile]
-        elif self._get_version() > 6:
+        elif self.__version > 6:
             return [executable] + options + ["-p", task.property_file, sourcefile]
-        assert False, "Unexpected version " + self._get_version()
+        assert False, "Unexpected version " + self.__version
 
     def determine_result(self, run):
         output = run.output
@@ -87,7 +76,7 @@ def determine_result(self, run):
         output = output[-1].strip()
         status = result.RESULT_UNKNOWN
 
-        if self._get_version() > 6:
+        if self.__version > 6:
             if output.endswith("TRUE"):
                 status = result.RESULT_TRUE_PROP
             elif "FALSE" in output:
@@ -110,7 +99,7 @@ def determine_result(self, run):
             else:
                 status = "ERROR"
 
-        elif self._get_version() == 6:
+        elif self.__version == 6:
             if output.endswith("TRUE"):
                 status = result.RESULT_TRUE_PROP
             elif "FALSE" in output:
diff --git a/benchexec/tools/symbiotic.py b/benchexec/tools/symbiotic.py
index 282cebaa6..330faa344 100644
--- a/benchexec/tools/symbiotic.py
+++ b/benchexec/tools/symbiotic.py
@@ -32,14 +32,14 @@ def executable(self, tool_locator):
         and most implementations will look similar to this one.
         The path returned should be relative to the current directory.
         """
-        # This is used in the function _version_newer_than.
-        # I don't know a better way to do it.
-        self.tool_locator = tool_locator
         try:
-            return tool_locator.find_executable("symbiotic", subdir="bin")
+            executable = tool_locator.find_executable("symbiotic", subdir="bin")
         except ToolNotFoundException:
             # this may be the old version of Symbiotic
-            return OldSymbiotic.executable(self, tool_locator)
+            executable = OldSymbiotic.executable(self, tool_locator)
+
+        self.__version = self.version(executable)
+        return executable
 
     def program_files(self, executable):
         if self._version_newer_than("7.0.0"):
@@ -61,8 +61,7 @@ def _version_newer_than(self, vers):
         """
         Determine whether the version is greater than some given version
         """
-        v = self.version(self.executable(self.tool_locator))
-        vers_num = v[: v.index("-")]
+        vers_num = self.__version[: self.__version.index("-")]
         if not vers_num[0].isdigit():
             # this is the old version which is "older" than any given version
             return False

From 2b4a6a1fbf69d98062f433ab690e55db316abb02 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Mon, 26 Oct 2020 11:44:40 +0100
Subject: [PATCH 18/46] updated two_ls: replaced length check on run.output

---
 benchexec/tools/two_ls.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/benchexec/tools/two_ls.py b/benchexec/tools/two_ls.py
index 08bfe2e6f..77b748577 100644
--- a/benchexec/tools/two_ls.py
+++ b/benchexec/tools/two_ls.py
@@ -50,7 +50,7 @@ def determine_result(self, run):
         elif returncode == 0:
             status = result.RESULT_TRUE_PROP
         elif returncode == 10:
-            if len(run.output) > 0:
+            if run.output:
                 result_str = run.output[-1].strip()
                 if result_str == "FALSE(valid-memtrack)":
                     status = result.RESULT_FALSE_MEMTRACK

From b28f883d752cc0656615bceae0bf4a5d0eeedc08 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Mon, 26 Oct 2020 11:46:44 +0100
Subject: [PATCH 19/46] updated symbiotic: replaced None check for run.output

---
 benchexec/tools/symbiotic.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/benchexec/tools/symbiotic.py b/benchexec/tools/symbiotic.py
index 330faa344..6838e5c57 100644
--- a/benchexec/tools/symbiotic.py
+++ b/benchexec/tools/symbiotic.py
@@ -107,7 +107,7 @@ def determine_result(self, run):
         returnsignal = run.exit_code.signal or 0
         returncode = run.exit_code.value or 0
 
-        if run.output is None:
+        if not run.output:
             return "{0}(no output)".format(result.RESULT_ERROR)
 
         if self._version_newer_than("4.0.1"):

From 0881f10ea6766fae70fd9dbf5696d5c8e8e7eb22 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Mon, 26 Oct 2020 11:59:14 +0100
Subject: [PATCH 20/46] updated predatorHP: data model param

---
 benchexec/tools/predatorhp.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/benchexec/tools/predatorhp.py b/benchexec/tools/predatorhp.py
index 72157862b..3bd78c116 100644
--- a/benchexec/tools/predatorhp.py
+++ b/benchexec/tools/predatorhp.py
@@ -35,10 +35,11 @@ def cmdline(self, executable, options, task, rlimits):
         )
 
         data_model_param = util.get_data_model_from_task(
-            task, {"ILP32": "-m32", "LP64": "-m64"}
+            task,
+            {"ILP32": "--compiler-options=-m32", "LP64": "--compiler-options=-m64"},
         )
         if data_model_param and data_model_param not in options:
-            options += ["--compiler-options", data_model_param]
+            options += [data_model_param]
 
         return [executable] + options + spec + list(task.input_files_or_identifier)
 

From f86559fb27bf6844cf5515dba93b021247b2aeeb Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Mon, 26 Oct 2020 12:01:32 +0100
Subject: [PATCH 21/46] updated cseq and predatorhp: using
 run.output.any_line_contains

---
 benchexec/tools/cseq.py       |  5 ++---
 benchexec/tools/predatorhp.py | 15 +++++++--------
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/benchexec/tools/cseq.py b/benchexec/tools/cseq.py
index 587367b09..357983178 100644
--- a/benchexec/tools/cseq.py
+++ b/benchexec/tools/cseq.py
@@ -43,11 +43,10 @@ def cmdline(self, executable, options, task, rlimits):
         return [executable] + options + spec + inputfile
 
     def determine_result(self, run):
-        output = "\n".join(run.output)
         status = result.RESULT_UNKNOWN
-        if "FALSE" in output:
+        if run.output.any_line_contains("FALSE"):
             status = result.RESULT_FALSE_REACH
-        elif "TRUE" in output:
+        elif run.output.any_line_contains("TRUE"):
             status = result.RESULT_TRUE_PROP
         else:
             status = result.RESULT_UNKNOWN
diff --git a/benchexec/tools/predatorhp.py b/benchexec/tools/predatorhp.py
index 3bd78c116..f9edcfbf5 100644
--- a/benchexec/tools/predatorhp.py
+++ b/benchexec/tools/predatorhp.py
@@ -44,21 +44,20 @@ def cmdline(self, executable, options, task, rlimits):
         return [executable] + options + spec + list(task.input_files_or_identifier)
 
     def determine_result(self, run):
-        output = "\n".join(run.output)
         status = "UNKNOWN"
-        if "UNKNOWN" in output:
+        if run.output.any_line_contains("UNKNOWN"):
             status = result.RESULT_UNKNOWN
-        elif "TRUE" in output:
+        elif run.output.any_line_contains("TRUE"):
             status = result.RESULT_TRUE_PROP
-        elif "FALSE(valid-memtrack)" in output:
+        elif run.output.any_line_contains("FALSE(valid-memtrack)"):
             status = result.RESULT_FALSE_MEMTRACK
-        elif "FALSE(valid-deref)" in output:
+        elif run.output.any_line_contains("FALSE(valid-deref)"):
             status = result.RESULT_FALSE_DEREF
-        elif "FALSE(valid-free)" in output:
+        elif run.output.any_line_contains("FALSE(valid-free)"):
             status = result.RESULT_FALSE_FREE
-        elif "FALSE(valid-memcleanup)" in output:
+        elif run.output.any_line_contains("FALSE(valid-memcleanup)"):
             status = result.RESULT_FALSE_MEMCLEANUP
-        elif "FALSE" in output:
+        elif run.output.any_line_contains("FALSE"):
             status = result.RESULT_FALSE_REACH
         if status == "UNKNOWN" and run.was_timeout:
             status = "TIMEOUT"

From f2d7b96e04126b075a70bf66ecc07b64b0be151e Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Mon, 26 Oct 2020 13:48:14 +0100
Subject: [PATCH 22/46] updated divine tools: using previous style returncode

---
 benchexec/tools/divine.py  | 3 ++-
 benchexec/tools/divine4.py | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/benchexec/tools/divine.py b/benchexec/tools/divine.py
index 99ee5b8f4..7d4a63cfc 100644
--- a/benchexec/tools/divine.py
+++ b/benchexec/tools/divine.py
@@ -96,6 +96,7 @@ def determine_result(self, run):
         and should give some indication of the failure reason
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
         """
+        returncode = run.exit_code.value or 0
 
         if not run.output:
             return "ERROR - no output"
@@ -105,7 +106,7 @@ def determine_result(self, run):
         if run.was_timeout:
             return "TIMEOUT"
 
-        if run.exit_code.value != 0:
+        if returncode != 0:
             return "ERROR - Pre-run"
 
         if last is None:
diff --git a/benchexec/tools/divine4.py b/benchexec/tools/divine4.py
index 743721eed..c82177818 100644
--- a/benchexec/tools/divine4.py
+++ b/benchexec/tools/divine4.py
@@ -94,6 +94,7 @@ def determine_result(self, run):
         and should give some indication of the failure reason
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
         """
+        returncode = run.exit_code.value or 0
 
         if not run.output:
             return "ERROR - no output"
@@ -103,7 +104,7 @@ def determine_result(self, run):
         if run.was_timeout:
             return "TIMEOUT"
 
-        if run.exit_code.value != 0:
+        if returncode != 0:
             return "ERROR - {0}".format(last)
 
         if "result:" in last:

From 0af3679ba62ae7f83a8d5d7277ea12c9a35df353 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Mon, 26 Oct 2020 13:58:14 +0100
Subject: [PATCH 23/46] updated brick: remove use of run.output._lines

---
 benchexec/tools/brick.py | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/benchexec/tools/brick.py b/benchexec/tools/brick.py
index 0103f563c..8b03d1d4b 100644
--- a/benchexec/tools/brick.py
+++ b/benchexec/tools/brick.py
@@ -45,17 +45,14 @@ def program_files(self, executable):
     def determine_result(self, run):
         status = result.RESULT_ERROR
 
-        for line in run.output._lines:
-            if line == "VERIFICATION SUCCESSFUL\n":
+        for line in run.output:
+            if line == "VERIFICATION SUCCESSFUL":
                 status = result.RESULT_TRUE_PROP
                 break
-            elif line == "VERIFICATION FAILED\n":
+            elif line == "VERIFICATION FAILED":
                 status = result.RESULT_FALSE_REACH
                 break
-            elif (
-                line == "VERIFICATION UNKNOWN\n"
-                or line == "VERIFICATION BOUNDED TRUE\n"
-            ):
+            elif line == "VERIFICATION UNKNOWN" or line == "VERIFICATION BOUNDED TRUE":
                 status = result.RESULT_UNKNOWN
                 break
 

From fc874d47b6d1a031f0cc7403a0ebf0706670ceea Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Mon, 26 Oct 2020 14:43:26 +0100
Subject: [PATCH 24/46] updated gacal, verifuzz and esbmc: using the flag to
 check the options

---
 benchexec/tools/esbmc.py    | 2 +-
 benchexec/tools/gacal.py    | 2 +-
 benchexec/tools/verifuzz.py | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/benchexec/tools/esbmc.py b/benchexec/tools/esbmc.py
index 3523c93b9..88188b963 100644
--- a/benchexec/tools/esbmc.py
+++ b/benchexec/tools/esbmc.py
@@ -39,7 +39,7 @@ def cmdline(self, executable, options, task, rlimits):
         data_model_param = util.get_data_model_from_task(
             task, {"ILP32": "32", "LP64": "64"}
         )
-        if data_model_param and data_model_param not in options:
+        if data_model_param and "--arch" not in options:
             options += ["--arch", data_model_param]
         return [executable] + ["-p", task.property_file] + options + [inputfile]
 
diff --git a/benchexec/tools/gacal.py b/benchexec/tools/gacal.py
index 3c96cbaef..2334dad1e 100644
--- a/benchexec/tools/gacal.py
+++ b/benchexec/tools/gacal.py
@@ -38,7 +38,7 @@ def cmdline(self, executable, options, task, rlimits):
         data_model_param = util.get_data_model_from_task(
             task, {"ILP32": "32", "LP64": "64"}
         )
-        if data_model_param and data_model_param not in options:
+        if data_model_param and "--architecture" not in options:
             options += ["--architecture", data_model_param]
 
         return [executable] + options + list(task.input_files_or_identifier)
diff --git a/benchexec/tools/verifuzz.py b/benchexec/tools/verifuzz.py
index 4e69f31d2..2925a3031 100644
--- a/benchexec/tools/verifuzz.py
+++ b/benchexec/tools/verifuzz.py
@@ -48,7 +48,7 @@ def cmdline(self, executable, options, task, rlimits):
         data_model_param = util.get_data_model_from_task(
             task, {"ILP32": "32", "LP64": "64"}
         )
-        if data_model_param and data_model_param not in options:
+        if data_model_param and "--bit" not in options:
             options += ["--bit", data_model_param]
 
         return [executable] + options + [task.single_input_file]

From 5ff4a73179ffa7dcb5ac07972f59ca1809f6d436 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Mon, 26 Oct 2020 17:16:51 +0100
Subject: [PATCH 25/46] using exit_code.signal instead of returnsignal

---
 benchexec/tools/cbmc.py                | 3 +--
 benchexec/tools/fshell-witness2test.py | 3 +--
 benchexec/tools/pinaka.py              | 3 +--
 benchexec/tools/symbiotic.py           | 5 ++---
 benchexec/tools/two_ls.py              | 9 ++++-----
 5 files changed, 9 insertions(+), 14 deletions(-)

diff --git a/benchexec/tools/cbmc.py b/benchexec/tools/cbmc.py
index dc14a17ef..ec7b076cb 100644
--- a/benchexec/tools/cbmc.py
+++ b/benchexec/tools/cbmc.py
@@ -109,11 +109,10 @@ def isErrorMessage(msg):
         return status
 
     def determine_result(self, run):
-        returnsignal = run.exit_code.signal or 0
         returncode = run.exit_code.value or 0
         output = run.output
 
-        if returnsignal == 0 and ((returncode == 0) or (returncode == 10)):
+        if not run.exit_code.signal and ((returncode == 0) or (returncode == 10)):
             status = result.RESULT_ERROR
             if "--xml-ui" in self.options:
                 status = self.parse_XML(output, returncode, run.was_timeout)
diff --git a/benchexec/tools/fshell-witness2test.py b/benchexec/tools/fshell-witness2test.py
index 8f76ba270..0ca6eded5 100644
--- a/benchexec/tools/fshell-witness2test.py
+++ b/benchexec/tools/fshell-witness2test.py
@@ -87,11 +87,10 @@ def determine_result(self, run):
         (useful to distinguish between program killed because of error and timeout)
         @return a non-empty string, usually one of the benchexec.result.RESULT_* constants
         """
-        returnsignal = run.exit_code.signal or 0
         returncode = run.exit_code.value or 0
         output = run.output
         status = result.RESULT_ERROR
-        if returnsignal == 0 and returncode == 0:
+        if not run.exit_code.signal and returncode == 0:
             if output:
                 result_str = output[-1].strip()
 
diff --git a/benchexec/tools/pinaka.py b/benchexec/tools/pinaka.py
index 720dde045..79486c8e3 100644
--- a/benchexec/tools/pinaka.py
+++ b/benchexec/tools/pinaka.py
@@ -35,12 +35,11 @@ def cmdline(self, executable, options, task, rlimits):
         return [executable] + options + list(task.input_files_or_identifier)
 
     def determine_result(self, run):
-        returnsignal = run.exit_code.signal or 0
         returncode = run.exit_code.value or 0
         output = run.output._lines
         status = ""
 
-        if returnsignal == 0 and ((returncode == 0) or (returncode == 10)):
+        if not run.exit_code.signal and ((returncode == 0) or (returncode == 10)):
             if "VERIFICATION FAILED (ReachSafety)\n" in output:
                 status = result.RESULT_FALSE_REACH
             elif "VERIFICATION FAILED (NoOverflow)\n" in output:
diff --git a/benchexec/tools/symbiotic.py b/benchexec/tools/symbiotic.py
index 6838e5c57..291451dfe 100644
--- a/benchexec/tools/symbiotic.py
+++ b/benchexec/tools/symbiotic.py
@@ -104,7 +104,6 @@ def _getPhase(self, output):
         return lastphase
 
     def determine_result(self, run):
-        returnsignal = run.exit_code.signal or 0
         returncode = run.exit_code.value or 0
 
         if not run.output:
@@ -139,9 +138,9 @@ def determine_result(self, run):
 
         if run.was_timeout:
             return self._getPhase(run.output)  # generates TIMEOUT(phase)
-        elif returnsignal != 0:
+        elif run.exit_code.signal:
             return "KILLED (signal {0}, {1})".format(
-                returnsignal, self._getPhase(run.output)
+                run.exit_code.signal, self._getPhase(run.output)
             )
         elif returncode != 0:
             return "{0}(returned {1}, {2})".format(
diff --git a/benchexec/tools/two_ls.py b/benchexec/tools/two_ls.py
index 77b748577..6338b9f37 100644
--- a/benchexec/tools/two_ls.py
+++ b/benchexec/tools/two_ls.py
@@ -39,14 +39,13 @@ def cmdline(self, executable, options, task, rlimits):
         return [executable] + options + list(task.input_files_or_identifier)
 
     def determine_result(self, run):
-        returnsignal = run.exit_code.signal or 0
         returncode = run.exit_code.value or 0
-        if ((returnsignal == 9) or (returnsignal == 15)) and run.was_timeout:
+        if ((run.exit_code.signal == 9) or (run.exit_code.signal == 15)) and run.was_timeout:
             status = "TIMEOUT"
-        elif returnsignal == 9:
+        elif run.exit_code.signal == 9:
             status = "OUT OF MEMORY"
-        elif returnsignal != 0:
-            status = "ERROR(SIGNAL " + str(returnsignal) + ")"
+        elif run.exit_code.signal:
+            status = "ERROR(SIGNAL " + str(run.exit_code.signal) + ")"
         elif returncode == 0:
             status = result.RESULT_TRUE_PROP
         elif returncode == 10:

From 5823bfb9ed00b07a19413ae454100020ee3a5bfa Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Tue, 27 Oct 2020 10:35:09 +0100
Subject: [PATCH 26/46] using exit_code.value instead of returncode

---
 benchexec/tools/cbmc.py                | 19 +++++++++----------
 benchexec/tools/divine.py              |  4 +---
 benchexec/tools/divine4.py             |  4 ++--
 benchexec/tools/fshell-witness2test.py |  7 +++----
 benchexec/tools/pinaka.py              |  3 +--
 benchexec/tools/symbiotic.py           |  6 ++----
 benchexec/tools/two_ls.py              |  9 +++++----
 7 files changed, 23 insertions(+), 29 deletions(-)

diff --git a/benchexec/tools/cbmc.py b/benchexec/tools/cbmc.py
index ec7b076cb..164ae8baf 100644
--- a/benchexec/tools/cbmc.py
+++ b/benchexec/tools/cbmc.py
@@ -48,7 +48,7 @@ def cmdline(self, executable, options, task, rlimits):
 
         return [executable] + options + list(task.input_files_or_identifier)
 
-    def parse_XML(self, output, returncode, isTimeout):
+    def parse_XML(self, output, exit_code, isTimeout):
         # an empty tag cannot be parsed into a tree
         def sanitizeXML(s):
             return s.replace("<>", "<emptyTag>").replace("</>", "</emptyTag>")
@@ -78,7 +78,7 @@ def isErrorMessage(msg):
                     status = "INVALID OUTPUT"
 
             elif status == "FAILURE":
-                assert returncode == 10
+                assert exit_code.value == 10
                 reason = tree.find("goto_trace").find("failure").findtext("reason")
                 if not reason:
                     reason = tree.find("goto_trace").find("failure").get("reason")
@@ -88,7 +88,7 @@ def isErrorMessage(msg):
                     status = result.RESULT_FALSE_REACH
 
             elif status == "SUCCESS":
-                assert returncode == 0
+                assert exit_code.value == 0
                 if "--unwinding-assertions" in self.options:
                     status = result.RESULT_TRUE_PROP
                 else:
@@ -103,19 +103,18 @@ def isErrorMessage(msg):
             else:
                 status = "INVALID OUTPUT"
                 logging.exception(
-                    "Error parsing CBMC output for returncode %d", returncode
+                    "Error parsing CBMC output for exit_code.value %d", exit_code.value
                 )
 
         return status
 
     def determine_result(self, run):
-        returncode = run.exit_code.value or 0
         output = run.output
 
-        if not run.exit_code.signal and ((returncode == 0) or (returncode == 10)):
+        if run.exit_code.value in [0, 10]:
             status = result.RESULT_ERROR
             if "--xml-ui" in self.options:
-                status = self.parse_XML(output, returncode, run.was_timeout)
+                status = self.parse_XML(output, run.exit_code.value, run.was_timeout)
             elif len(output) > 0:
                 # SV-COMP mode
                 result_str = output[-1].strip()
@@ -138,13 +137,13 @@ def determine_result(self, run):
                 elif "UNKNOWN" in output:
                     status = result.RESULT_UNKNOWN
 
-        elif returncode == 64 and "Usage error!\n" in output:
+        elif run.exit_code.value == 64 and "Usage error!\n" in output:
             status = "INVALID ARGUMENTS"
 
-        elif returncode == 6 and "Out of memory\n" in output:
+        elif run.exit_code.value == 6 and "Out of memory\n" in output:
             status = "OUT OF MEMORY"
 
-        elif returncode == 6 and "SAT checker ran out of memory\n" in output:
+        elif run.exit_code.value == 6 and "SAT checker ran out of memory\n" in output:
             status = "OUT OF MEMORY"
 
         else:
diff --git a/benchexec/tools/divine.py b/benchexec/tools/divine.py
index 7d4a63cfc..627989790 100644
--- a/benchexec/tools/divine.py
+++ b/benchexec/tools/divine.py
@@ -96,8 +96,6 @@ def determine_result(self, run):
         and should give some indication of the failure reason
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
         """
-        returncode = run.exit_code.value or 0
-
         if not run.output:
             return "ERROR - no output"
 
@@ -106,7 +104,7 @@ def determine_result(self, run):
         if run.was_timeout:
             return "TIMEOUT"
 
-        if returncode != 0:
+        if run.exit_code.value != 0:
             return "ERROR - Pre-run"
 
         if last is None:
diff --git a/benchexec/tools/divine4.py b/benchexec/tools/divine4.py
index c82177818..999f8506e 100644
--- a/benchexec/tools/divine4.py
+++ b/benchexec/tools/divine4.py
@@ -94,7 +94,7 @@ def determine_result(self, run):
         and should give some indication of the failure reason
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
         """
-        returncode = run.exit_code.value or 0
+        run.exit_code.value = run.exit_code.value or 0
 
         if not run.output:
             return "ERROR - no output"
@@ -104,7 +104,7 @@ def determine_result(self, run):
         if run.was_timeout:
             return "TIMEOUT"
 
-        if returncode != 0:
+        if run.exit_code.value != 0:
             return "ERROR - {0}".format(last)
 
         if "result:" in last:
diff --git a/benchexec/tools/fshell-witness2test.py b/benchexec/tools/fshell-witness2test.py
index 0ca6eded5..06facf28c 100644
--- a/benchexec/tools/fshell-witness2test.py
+++ b/benchexec/tools/fshell-witness2test.py
@@ -80,17 +80,16 @@ def determine_result(self, run):
         Otherwise an arbitrary string can be returned that will be shown to the user
         and should give some indication of the failure reason
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
-        @param returncode: the exit code of the program, 0 if the program was killed
-        @param returnsignal: the signal that killed the program, 0 if program exited itself
+        @param run.exit_code.value: the exit code of the program, None if the program was killed
+        @param runb.exi_code.signal: the signal that killed the program, None if program exited itself
         @param output: a list of strings of output lines of the tool (both stdout and stderr)
         @param isTimeout: whether the result is a timeout
         (useful to distinguish between program killed because of error and timeout)
         @return a non-empty string, usually one of the benchexec.result.RESULT_* constants
         """
-        returncode = run.exit_code.value or 0
         output = run.output
         status = result.RESULT_ERROR
-        if not run.exit_code.signal and returncode == 0:
+        if run.exit_code.value == 0:
             if output:
                 result_str = output[-1].strip()
 
diff --git a/benchexec/tools/pinaka.py b/benchexec/tools/pinaka.py
index 79486c8e3..c423d213a 100644
--- a/benchexec/tools/pinaka.py
+++ b/benchexec/tools/pinaka.py
@@ -35,11 +35,10 @@ def cmdline(self, executable, options, task, rlimits):
         return [executable] + options + list(task.input_files_or_identifier)
 
     def determine_result(self, run):
-        returncode = run.exit_code.value or 0
         output = run.output._lines
         status = ""
 
-        if not run.exit_code.signal and ((returncode == 0) or (returncode == 10)):
+        if run.exit_code.value in [0, 10]:
             if "VERIFICATION FAILED (ReachSafety)\n" in output:
                 status = result.RESULT_FALSE_REACH
             elif "VERIFICATION FAILED (NoOverflow)\n" in output:
diff --git a/benchexec/tools/symbiotic.py b/benchexec/tools/symbiotic.py
index 291451dfe..a56fda24a 100644
--- a/benchexec/tools/symbiotic.py
+++ b/benchexec/tools/symbiotic.py
@@ -104,8 +104,6 @@ def _getPhase(self, output):
         return lastphase
 
     def determine_result(self, run):
-        returncode = run.exit_code.value or 0
-
         if not run.output:
             return "{0}(no output)".format(result.RESULT_ERROR)
 
@@ -142,9 +140,9 @@ def determine_result(self, run):
             return "KILLED (signal {0}, {1})".format(
                 run.exit_code.signal, self._getPhase(run.output)
             )
-        elif returncode != 0:
+        elif run.exit_code.value != 0:
             return "{0}(returned {1}, {2})".format(
-                result.RESULT_ERROR, returncode, self._getPhase(run.output)
+                result.RESULT_ERROR, run.exit_code.value, self._getPhase(run.output)
             )
 
         return "{0}(unknown, {1})".format(
diff --git a/benchexec/tools/two_ls.py b/benchexec/tools/two_ls.py
index 6338b9f37..1a42244b5 100644
--- a/benchexec/tools/two_ls.py
+++ b/benchexec/tools/two_ls.py
@@ -39,16 +39,17 @@ def cmdline(self, executable, options, task, rlimits):
         return [executable] + options + list(task.input_files_or_identifier)
 
     def determine_result(self, run):
-        returncode = run.exit_code.value or 0
-        if ((run.exit_code.signal == 9) or (run.exit_code.signal == 15)) and run.was_timeout:
+        if (
+            (run.exit_code.signal == 9) or (run.exit_code.signal == 15)
+        ) and run.was_timeout:
             status = "TIMEOUT"
         elif run.exit_code.signal == 9:
             status = "OUT OF MEMORY"
         elif run.exit_code.signal:
             status = "ERROR(SIGNAL " + str(run.exit_code.signal) + ")"
-        elif returncode == 0:
+        elif run.exit_code.value == 0:
             status = result.RESULT_TRUE_PROP
-        elif returncode == 10:
+        elif run.exit_code.value == 10:
             if run.output:
                 result_str = run.output[-1].strip()
                 if result_str == "FALSE(valid-memtrack)":

From 6b526edc4561f9c86b55b7b52dbca0621a9c287b Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Tue, 27 Oct 2020 12:57:07 +0100
Subject: [PATCH 27/46] using task.single_input_file in cseq, esbmc, map2check

---
 benchexec/tools/cseq.py      | 10 +++-------
 benchexec/tools/esbmc.py     | 11 ++++++-----
 benchexec/tools/map2check.py | 16 ++++++++++------
 3 files changed, 19 insertions(+), 18 deletions(-)

diff --git a/benchexec/tools/cseq.py b/benchexec/tools/cseq.py
index 357983178..44941be5d 100644
--- a/benchexec/tools/cseq.py
+++ b/benchexec/tools/cseq.py
@@ -29,18 +29,14 @@ def cmdline(self, executable, options, task, rlimits):
         are either absolute or have been made relative to the designated working directory.
         @param executable: the path to the executable of the tool (typically the result of executable())
         @param options: a list of options, in the same order as given in the XML-file.
-        @param tasks: a list of tasks, that should be analysed with the tool in one run.
-                            In most cases we we have only _one_ inputfile.
-        @param propertyfile: contains a specification for the verifier.
+        @param tasks: instance of class Task containg the property and input file
+                            This tool info module only supports one input file.
         @param rlimits: This dictionary contains resource-limits for a run,
                         for example: time-limit, soft-time-limit, hard-time-limit, memory-limit, cpu-core-limit.
                         All entries in rlimits are optional, so check for existence before usage!
         """
-        tasks = list(task.input_files_or_identifier)
-        assert len(tasks) == 1, "only one inputfile supported"
-        inputfile = ["--input", tasks[0]]
         spec = ["--spec", task.property_file] if task.property_file is not None else []
-        return [executable] + options + spec + inputfile
+        return [executable] + options + spec + ["--input", task.single_input_file]
 
     def determine_result(self, run):
         status = result.RESULT_UNKNOWN
diff --git a/benchexec/tools/esbmc.py b/benchexec/tools/esbmc.py
index 88188b963..c94d5243c 100644
--- a/benchexec/tools/esbmc.py
+++ b/benchexec/tools/esbmc.py
@@ -32,16 +32,17 @@ def name(self):
         return "ESBMC"
 
     def cmdline(self, executable, options, task, rlimits):
-        tasks = list(task.input_files_or_identifier)
-        assert len(tasks) == 1, "only one inputfile supported"
-        inputfile = tasks[0]
-
         data_model_param = util.get_data_model_from_task(
             task, {"ILP32": "32", "LP64": "64"}
         )
         if data_model_param and "--arch" not in options:
             options += ["--arch", data_model_param]
-        return [executable] + ["-p", task.property_file] + options + [inputfile]
+        return (
+            [executable]
+            + ["-p", task.property_file]
+            + options
+            + [task.single_input_file]
+        )
 
     def determine_result(self, run):
         output = "\n".join(run.output)
diff --git a/benchexec/tools/map2check.py b/benchexec/tools/map2check.py
index e00137adf..5e9b1b137 100644
--- a/benchexec/tools/map2check.py
+++ b/benchexec/tools/map2check.py
@@ -57,16 +57,20 @@ def name(self):
         return "Map2Check"
 
     def cmdline(self, executable, options, task, rlimits):
-        sourcefiles = list(task.input_files_or_identifier)
-
-        assert len(sourcefiles) == 1, "only one sourcefile supported"
         assert task.property_file, "property file required"
 
-        sourcefile = sourcefiles[0]
         if self.__version == 6:
-            return [executable] + options + ["-c", task.property_file, sourcefile]
+            return (
+                [executable]
+                + options
+                + ["-c", task.property_file, task.single_input_file]
+            )
         elif self.__version > 6:
-            return [executable] + options + ["-p", task.property_file, sourcefile]
+            return (
+                [executable]
+                + options
+                + ["-p", task.property_file, task.single_input_file]
+            )
         assert False, "Unexpected version " + self.__version
 
     def determine_result(self, run):

From 14cd4fc0477b9443c6b58a4824273510afdf076e Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Tue, 27 Oct 2020 14:19:57 +0100
Subject: [PATCH 28/46] moved get_data_model_from_task from util to
 sv_benchmarks_util

---
 benchexec/tools/brick.py               |  4 ++--
 benchexec/tools/cbmc.py                |  4 ++--
 benchexec/tools/divine.py              |  4 ++--
 benchexec/tools/divine4.py             |  4 ++--
 benchexec/tools/esbmc.py               |  6 ++----
 benchexec/tools/fshell-witness2test.py |  4 ++--
 benchexec/tools/gacal.py               |  6 ++----
 benchexec/tools/pinaka.py              |  4 ++--
 benchexec/tools/predatorhp.py          |  4 ++--
 benchexec/tools/sv_benchmarks_util.py  | 28 ++++++++++++++++++++++++++
 benchexec/tools/symbiotic4.py          |  4 ++--
 benchexec/tools/two_ls.py              |  4 ++--
 benchexec/tools/verifuzz.py            |  6 ++----
 benchexec/util.py                      | 19 -----------------
 14 files changed, 52 insertions(+), 49 deletions(-)
 create mode 100644 benchexec/tools/sv_benchmarks_util.py

diff --git a/benchexec/tools/brick.py b/benchexec/tools/brick.py
index 8b03d1d4b..b64713ad3 100644
--- a/benchexec/tools/brick.py
+++ b/benchexec/tools/brick.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -25,7 +25,7 @@ def name(self):
         return "BRICK"
 
     def cmdline(self, executable, options, task, rlimits):
-        data_model_param = util.get_data_model_from_task(
+        data_model_param = get_data_model_from_task(
             task, {"ILP32": "--32", "LP64": "--64"}
         )
         if data_model_param and data_model_param not in options:
diff --git a/benchexec/tools/cbmc.py b/benchexec/tools/cbmc.py
index 164ae8baf..55fae1544 100644
--- a/benchexec/tools/cbmc.py
+++ b/benchexec/tools/cbmc.py
@@ -8,7 +8,7 @@
 import logging
 from xml.etree import ElementTree
 
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -38,7 +38,7 @@ def cmdline(self, executable, options, task, rlimits):
         elif "--xml-ui" not in options:
             options = options + ["--xml-ui"]
 
-        data_model_param = util.get_data_model_from_task(
+        data_model_param = get_data_model_from_task(
             task, {"ILP32": "--32", "LP64": "--64"}
         )
         if data_model_param and data_model_param not in options:
diff --git a/benchexec/tools/divine.py b/benchexec/tools/divine.py
index 627989790..330766a2a 100644
--- a/benchexec/tools/divine.py
+++ b/benchexec/tools/divine.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -70,7 +70,7 @@ def cmdline(self, executable, options, task, rlimits):
                         for example: time-limit, soft-time-limit, hard-time-limit, memory-limit, cpu-core-limit.
                         All entries in rlimits are optional, so check for existence before usage!
         """
-        data_model_param = util.get_data_model_from_task(
+        data_model_param = get_data_model_from_task(
             task, {"ILP32": "--32", "LP64": "--64"}
         )
         if data_model_param and data_model_param not in options:
diff --git a/benchexec/tools/divine4.py b/benchexec/tools/divine4.py
index 999f8506e..34df27a8e 100644
--- a/benchexec/tools/divine4.py
+++ b/benchexec/tools/divine4.py
@@ -6,7 +6,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -68,7 +68,7 @@ def cmdline(self, executable, options, task, rlimits):
                         for example: time-limit, soft-time-limit, hard-time-limit, memory-limit, cpu-core-limit.
                         All entries in rlimits are optional, so check for existence before usage!
         """
-        data_model_param = util.get_data_model_from_task(
+        data_model_param = get_data_model_from_task(
             task, {"ILP32": "--32", "LP64": "--64"}
         )
         if data_model_param and data_model_param not in options:
diff --git a/benchexec/tools/esbmc.py b/benchexec/tools/esbmc.py
index c94d5243c..d6258eedf 100644
--- a/benchexec/tools/esbmc.py
+++ b/benchexec/tools/esbmc.py
@@ -6,7 +6,7 @@
 # SPDX-License-Identifier: Apache-2.0
 
 import os
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -32,9 +32,7 @@ def name(self):
         return "ESBMC"
 
     def cmdline(self, executable, options, task, rlimits):
-        data_model_param = util.get_data_model_from_task(
-            task, {"ILP32": "32", "LP64": "64"}
-        )
+        data_model_param = get_data_model_from_task(task, {"ILP32": "32", "LP64": "64"})
         if data_model_param and "--arch" not in options:
             options += ["--arch", data_model_param]
         return (
diff --git a/benchexec/tools/fshell-witness2test.py b/benchexec/tools/fshell-witness2test.py
index 06facf28c..24c7a0fa7 100644
--- a/benchexec/tools/fshell-witness2test.py
+++ b/benchexec/tools/fshell-witness2test.py
@@ -9,7 +9,7 @@
 
 import benchexec.result as result
 import benchexec.tools.template
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 
 
 class Tool(benchexec.tools.template.BaseTool2):
@@ -63,7 +63,7 @@ def cmdline(self, executable, options, task, rlimits):
         if task.property_file:
             options = options + ["--propertyfile", task.property_file]
 
-        data_model_param = util.get_data_model_from_task(
+        data_model_param = get_data_model_from_task(
             task, {"ILP32": "-m32", "LP64": "-m64"}
         )
         if data_model_param and data_model_param not in options:
diff --git a/benchexec/tools/gacal.py b/benchexec/tools/gacal.py
index 2334dad1e..65c736f10 100644
--- a/benchexec/tools/gacal.py
+++ b/benchexec/tools/gacal.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -35,9 +35,7 @@ def version(self, executable):
         return self._version_from_tool(executable)
 
     def cmdline(self, executable, options, task, rlimits):
-        data_model_param = util.get_data_model_from_task(
-            task, {"ILP32": "32", "LP64": "64"}
-        )
+        data_model_param = get_data_model_from_task(task, {"ILP32": "32", "LP64": "64"})
         if data_model_param and "--architecture" not in options:
             options += ["--architecture", data_model_param]
 
diff --git a/benchexec/tools/pinaka.py b/benchexec/tools/pinaka.py
index c423d213a..b22a3676d 100644
--- a/benchexec/tools/pinaka.py
+++ b/benchexec/tools/pinaka.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -26,7 +26,7 @@ def name(self):
     def cmdline(self, executable, options, task, rlimits):
         if task.property_file:
             options = options + ["--propertyfile", task.property_file]
-        data_model_param = util.get_data_model_from_task(
+        data_model_param = get_data_model_from_task(
             task, {"ILP32": "--32", "LP64": "--64"}
         )
         if data_model_param and data_model_param not in options:
diff --git a/benchexec/tools/predatorhp.py b/benchexec/tools/predatorhp.py
index f9edcfbf5..77d74ba12 100644
--- a/benchexec/tools/predatorhp.py
+++ b/benchexec/tools/predatorhp.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -34,7 +34,7 @@ def cmdline(self, executable, options, task, rlimits):
             else []
         )
 
-        data_model_param = util.get_data_model_from_task(
+        data_model_param = get_data_model_from_task(
             task,
             {"ILP32": "--compiler-options=-m32", "LP64": "--compiler-options=-m64"},
         )
diff --git a/benchexec/tools/sv_benchmarks_util.py b/benchexec/tools/sv_benchmarks_util.py
new file mode 100644
index 000000000..563ebaf06
--- /dev/null
+++ b/benchexec/tools/sv_benchmarks_util.py
@@ -0,0 +1,28 @@
+# This file is part of BenchExec, a framework for reliable benchmarking:
+# https://github.com/sosy-lab/benchexec
+#
+# SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+"""
+This module contains some useful functions related to tasks in the sv-benchmarks
+repository: https://github.com/sosy-lab/sv-benchmarks
+"""
+
+import benchexec.tools.template
+
+def get_data_model_from_task(task, data_models):
+    if isinstance(task.options, dict) and task.options.get("language") == "C":
+        data_model = task.options.get("data_model")
+        if data_model:
+            data_model_option = data_models.get(data_model)
+            if data_model_option:
+                return data_model_option
+            else:
+                raise benchexec.tools.template.UnsupportedFeatureException(
+                    "Unsupported data_model '{}' defined for task '{}'".format(
+                        data_model, task
+                    )
+                )
+    return None
diff --git a/benchexec/tools/symbiotic4.py b/benchexec/tools/symbiotic4.py
index 0492e0e8e..bad5d4740 100644
--- a/benchexec/tools/symbiotic4.py
+++ b/benchexec/tools/symbiotic4.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -54,7 +54,7 @@ def cmdline(self, executable, options, task, rlimits):
         if task.property_file is not None:
             options = options + ["--prp={0}".format(task.property_file)]
 
-        data_model_param = util.get_data_model_from_task(
+        data_model_param = get_data_model_from_task(
             task, {"ILP32": "--32", "LP64": "--64"}
         )
         if data_model_param and data_model_param not in options:
diff --git a/benchexec/tools/two_ls.py b/benchexec/tools/two_ls.py
index 1a42244b5..e6e7cabc8 100644
--- a/benchexec/tools/two_ls.py
+++ b/benchexec/tools/two_ls.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -30,7 +30,7 @@ def cmdline(self, executable, options, task, rlimits):
         if task.property_file:
             options = options + ["--propertyfile", task.property_file]
 
-        data_model_param = util.get_data_model_from_task(
+        data_model_param = get_data_model_from_task(
             task, {"ILP32": "--32", "LP64": "--64"}
         )
         if data_model_param and data_model_param not in options:
diff --git a/benchexec/tools/verifuzz.py b/benchexec/tools/verifuzz.py
index 2925a3031..9a7822142 100644
--- a/benchexec/tools/verifuzz.py
+++ b/benchexec/tools/verifuzz.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -45,9 +45,7 @@ def cmdline(self, executable, options, task, rlimits):
         if task.property_file:
             options = options + ["--propertyFile", task.property_file]
 
-        data_model_param = util.get_data_model_from_task(
-            task, {"ILP32": "32", "LP64": "64"}
-        )
+        data_model_param = get_data_model_from_task(task, {"ILP32": "32", "LP64": "64"})
         if data_model_param and "--bit" not in options:
             options += ["--bit", data_model_param]
 
diff --git a/benchexec/util.py b/benchexec/util.py
index 6a42c2375..b2bd8f702 100644
--- a/benchexec/util.py
+++ b/benchexec/util.py
@@ -762,22 +762,3 @@ def check_msr():
         if all(os.access("/dev/cpu/{}/msr".format(cpu), os.W_OK) for cpu in cpu_dirs):
             res["write"] = True
     return res
-
-
-def get_data_model_from_task(task, data_models):
-    # Importing it here, otherwise it will result in cyclic dependency.
-    import benchexec.tools.template
-
-    if isinstance(task.options, dict) and task.options.get("language") == "C":
-        data_model = task.options.get("data_model")
-        if data_model:
-            data_model_option = data_models.get(data_model)
-            if data_model_option:
-                return data_model_option
-            else:
-                raise benchexec.tools.template.UnsupportedFeatureException(
-                    "Unsupported data_model '{}' defined for task '{}'".format(
-                        data_model, task
-                    )
-                )
-    return None

From ffc51e1ad5b4845898d44d7ef064ed0a4f070d0b Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Tue, 27 Oct 2020 15:24:16 +0100
Subject: [PATCH 29/46] fixed flake8 warning

---
 benchexec/tools/sv_benchmarks_util.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/benchexec/tools/sv_benchmarks_util.py b/benchexec/tools/sv_benchmarks_util.py
index 563ebaf06..c5ca1574c 100644
--- a/benchexec/tools/sv_benchmarks_util.py
+++ b/benchexec/tools/sv_benchmarks_util.py
@@ -12,6 +12,7 @@
 
 import benchexec.tools.template
 
+
 def get_data_model_from_task(task, data_models):
     if isinstance(task.options, dict) and task.options.get("language") == "C":
         data_model = task.options.get("data_model")

From af5bd81bdaf51faa9778931901fcbb1b5f251175 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Tue, 27 Oct 2020 15:47:27 +0100
Subject: [PATCH 30/46] removed _lines from pinaka

---
 benchexec/tools/pinaka.py | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/benchexec/tools/pinaka.py b/benchexec/tools/pinaka.py
index b22a3676d..7bdf424cc 100644
--- a/benchexec/tools/pinaka.py
+++ b/benchexec/tools/pinaka.py
@@ -35,15 +35,14 @@ def cmdline(self, executable, options, task, rlimits):
         return [executable] + options + list(task.input_files_or_identifier)
 
     def determine_result(self, run):
-        output = run.output._lines
         status = ""
 
         if run.exit_code.value in [0, 10]:
-            if "VERIFICATION FAILED (ReachSafety)\n" in output:
+            if run.output.any_line_contains("VERIFICATION FAILED (ReachSafety)"):
                 status = result.RESULT_FALSE_REACH
-            elif "VERIFICATION FAILED (NoOverflow)\n" in output:
+            elif run.output.any_line_contains("VERIFICATION FAILED (NoOverflow)"):
                 status = result.RESULT_FALSE_OVERFLOW
-            elif "VERIFICATION SUCCESSFUL\n" in output:
+            elif run.output.any_line_contains("VERIFICATION SUCCESSFUL"):
                 status = result.RESULT_TRUE_PROP
             else:
                 status = result.RESULT_UNKNOWN

From 4cf9ec8e54d8a90a314ac265d5cbbbdb589e8851 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Tue, 27 Oct 2020 19:27:08 +0100
Subject: [PATCH 31/46] using any_line_containts in esbmc

---
 benchexec/tools/esbmc.py | 32 +++++++++-----------------------
 1 file changed, 9 insertions(+), 23 deletions(-)

diff --git a/benchexec/tools/esbmc.py b/benchexec/tools/esbmc.py
index d6258eedf..42482f519 100644
--- a/benchexec/tools/esbmc.py
+++ b/benchexec/tools/esbmc.py
@@ -43,43 +43,29 @@ def cmdline(self, executable, options, task, rlimits):
         )
 
     def determine_result(self, run):
-        output = "\n".join(run.output)
         status = result.RESULT_UNKNOWN
 
-        if self.allInText(["FALSE_DEREF"], output):
+        if run.output.any_line_contains("FALSE_DEREF"):
             status = result.RESULT_FALSE_DEREF
-        elif self.allInText(["FALSE_FREE"], output):
+        elif run.output.any_line_contains("FALSE_FREE"):
             status = result.RESULT_FALSE_FREE
-        elif self.allInText(["FALSE_MEMTRACK"], output):
+        elif run.output.any_line_contains("FALSE_MEMTRACK"):
             status = result.RESULT_FALSE_MEMTRACK
-        elif self.allInText(["FALSE_OVERFLOW"], output):
+        elif run.output.any_line_contains("FALSE_OVERFLOW"):
             status = result.RESULT_FALSE_OVERFLOW
-        elif self.allInText(["FALSE_TERMINATION"], output):
+        elif run.output.any_line_contains("FALSE_TERMINATION"):
             status = result.RESULT_FALSE_TERMINATION
-        elif self.allInText(["FALSE"], output):
+        elif run.output.any_line_contains("FALSE"):
             status = result.RESULT_FALSE_REACH
-        elif "TRUE" in output:
+        elif run.output.any_line_contains("TRUE"):
             status = result.RESULT_TRUE_PROP
-        elif "DONE" in output:
+        elif run.output.any_line_contains("DONE"):
             status = result.RESULT_DONE
 
         if status == result.RESULT_UNKNOWN:
             if run.was_timeout:
                 status = "TIMEOUT"
-            elif output.endswith(("error", "error\n")):
+            elif run.output[-1].endswith("error"):
                 status = "ERROR"
 
         return status
-
-    """ helper method """
-
-    def allInText(self, words, text):
-        """
-        This function checks, if all the words appear in the given order in the text.
-        """
-        index = 0
-        for word in words:
-            index = text[index:].find(word)
-            if index == -1:
-                return False
-        return True

From 66eb7e734da93d400ad5e4745dbe7b45409bf451 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Tue, 27 Oct 2020 19:32:10 +0100
Subject: [PATCH 32/46] updated cseq, predatorHP, and symbiotic4: refactored a
 None check

---
 benchexec/tools/cseq.py       | 4 ++--
 benchexec/tools/predatorhp.py | 6 +-----
 benchexec/tools/symbiotic4.py | 2 +-
 3 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/benchexec/tools/cseq.py b/benchexec/tools/cseq.py
index 44941be5d..b516e5451 100644
--- a/benchexec/tools/cseq.py
+++ b/benchexec/tools/cseq.py
@@ -29,13 +29,13 @@ def cmdline(self, executable, options, task, rlimits):
         are either absolute or have been made relative to the designated working directory.
         @param executable: the path to the executable of the tool (typically the result of executable())
         @param options: a list of options, in the same order as given in the XML-file.
-        @param tasks: instance of class Task containg the property and input file
+        @param task: instance of class Task containg the property and input file
                             This tool info module only supports one input file.
         @param rlimits: This dictionary contains resource-limits for a run,
                         for example: time-limit, soft-time-limit, hard-time-limit, memory-limit, cpu-core-limit.
                         All entries in rlimits are optional, so check for existence before usage!
         """
-        spec = ["--spec", task.property_file] if task.property_file is not None else []
+        spec = ["--spec", task.property_file] if task.property_file else []
         return [executable] + options + spec + ["--input", task.single_input_file]
 
     def determine_result(self, run):
diff --git a/benchexec/tools/predatorhp.py b/benchexec/tools/predatorhp.py
index 77d74ba12..4910790b0 100644
--- a/benchexec/tools/predatorhp.py
+++ b/benchexec/tools/predatorhp.py
@@ -28,11 +28,7 @@ def version(self, executable):
         return self._version_from_tool(executable, use_stderr=True)
 
     def cmdline(self, executable, options, task, rlimits):
-        spec = (
-            ["--propertyfile", task.property_file]
-            if task.property_file is not None
-            else []
-        )
+        spec = ["--propertyfile", task.property_file] if task.property_file else []
 
         data_model_param = get_data_model_from_task(
             task,
diff --git a/benchexec/tools/symbiotic4.py b/benchexec/tools/symbiotic4.py
index bad5d4740..67164de22 100644
--- a/benchexec/tools/symbiotic4.py
+++ b/benchexec/tools/symbiotic4.py
@@ -51,7 +51,7 @@ def cmdline(self, executable, options, task, rlimits):
         Compose the command line to execute from the name of the executable
         """
 
-        if task.property_file is not None:
+        if task.property_file:
             options = options + ["--prp={0}".format(task.property_file)]
 
         data_model_param = get_data_model_from_task(

From 78f718139b1300c094474898e74de1173ee09417 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Tue, 27 Oct 2020 19:35:09 +0100
Subject: [PATCH 33/46] updated symbiotic4: rewrote None check for run.output

---
 benchexec/tools/symbiotic4.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/benchexec/tools/symbiotic4.py b/benchexec/tools/symbiotic4.py
index 67164de22..ee1109409 100644
--- a/benchexec/tools/symbiotic4.py
+++ b/benchexec/tools/symbiotic4.py
@@ -66,7 +66,7 @@ def determine_result(self, run):
         if run.was_timeout:
             return "timeout"
 
-        if run.output is None:
+        if not run.output:
             return "error (no output)"
 
         for line in run.output:

From f2608c929d1e7ee7f86f1fb5f2674486fe00a4cb Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Tue, 27 Oct 2020 19:41:12 +0100
Subject: [PATCH 34/46] renamed __version to _version

---
 benchexec/tools/map2check.py | 18 +++++++++---------
 benchexec/tools/symbiotic.py |  4 ++--
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/benchexec/tools/map2check.py b/benchexec/tools/map2check.py
index 5e9b1b137..26eabde18 100644
--- a/benchexec/tools/map2check.py
+++ b/benchexec/tools/map2check.py
@@ -28,10 +28,10 @@ class Tool(benchexec.tools.template.BaseTool2):
     def executable(self, tool_locator):
         try:
             executable = tool_locator.find_executable("map2check-wrapper.sh")
-            self.__version = 6
+            self._version = 6
         except ToolNotFoundException:
             executable = tool_locator.find_executable("map2check-wrapper.py")
-            self.__version = 7
+            self._version = 7
 
         return executable
 
@@ -39,9 +39,9 @@ def program_files(self, executable):
         """
         Determine the file paths to be adopted
         """
-        if self.__version == 6:
+        if self._version == 6:
             paths = self.REQUIRED_PATHS_6
-        elif self.__version > 6:
+        elif self._version > 6:
             paths = self.REQUIRED_PATHS_7_1
 
         return paths
@@ -59,19 +59,19 @@ def name(self):
     def cmdline(self, executable, options, task, rlimits):
         assert task.property_file, "property file required"
 
-        if self.__version == 6:
+        if self._version == 6:
             return (
                 [executable]
                 + options
                 + ["-c", task.property_file, task.single_input_file]
             )
-        elif self.__version > 6:
+        elif self._version > 6:
             return (
                 [executable]
                 + options
                 + ["-p", task.property_file, task.single_input_file]
             )
-        assert False, "Unexpected version " + self.__version
+        assert False, "Unexpected version " + self._version
 
     def determine_result(self, run):
         output = run.output
@@ -80,7 +80,7 @@ def determine_result(self, run):
         output = output[-1].strip()
         status = result.RESULT_UNKNOWN
 
-        if self.__version > 6:
+        if self._version > 6:
             if output.endswith("TRUE"):
                 status = result.RESULT_TRUE_PROP
             elif "FALSE" in output:
@@ -103,7 +103,7 @@ def determine_result(self, run):
             else:
                 status = "ERROR"
 
-        elif self.__version == 6:
+        elif self._version == 6:
             if output.endswith("TRUE"):
                 status = result.RESULT_TRUE_PROP
             elif "FALSE" in output:
diff --git a/benchexec/tools/symbiotic.py b/benchexec/tools/symbiotic.py
index a56fda24a..5be644830 100644
--- a/benchexec/tools/symbiotic.py
+++ b/benchexec/tools/symbiotic.py
@@ -38,7 +38,7 @@ def executable(self, tool_locator):
             # this may be the old version of Symbiotic
             executable = OldSymbiotic.executable(self, tool_locator)
 
-        self.__version = self.version(executable)
+        self._version = self.version(executable)
         return executable
 
     def program_files(self, executable):
@@ -61,7 +61,7 @@ def _version_newer_than(self, vers):
         """
         Determine whether the version is greater than some given version
         """
-        vers_num = self.__version[: self.__version.index("-")]
+        vers_num = self._version[: self._version.index("-")]
         if not vers_num[0].isdigit():
             # this is the old version which is "older" than any given version
             return False

From 17a2e3b2a01538ed191a4bc1bfdcbac73d025961 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Wed, 28 Oct 2020 08:56:34 +0100
Subject: [PATCH 35/46] updated TI for klee

---
 benchexec/tools/klee.py | 52 +++++++++++++++++++++--------------------
 1 file changed, 27 insertions(+), 25 deletions(-)

diff --git a/benchexec/tools/klee.py b/benchexec/tools/klee.py
index 45f623316..460bd8d4c 100644
--- a/benchexec/tools/klee.py
+++ b/benchexec/tools/klee.py
@@ -6,20 +6,20 @@
 # SPDX-License-Identifier: Apache-2.0
 
 import benchexec.result as result
-import benchexec.util as util
 import benchexec.tools.template
 import benchexec.model
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for KLEE (https://klee.github.io).
     """
 
     REQUIRED_PATHS = ["bin", "include", "klee_build", "libraries"]
 
-    def executable(self):
-        return util.find_executable("bin/klee")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("klee", subdir="bin")
 
     def program_files(self, executable):
         return self._program_files_from_executable(
@@ -45,30 +45,32 @@ def version(self, executable):
         version = self._version_from_tool(executable, line_prefix="KLEE")
         return version.split("(")[0].strip()
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
-        if propertyfile:
-            options += ["--property-file=" + propertyfile]
-        if benchexec.model.MEMLIMIT in rlimits:
-            options += ["--max-memory=" + str(rlimits[benchexec.model.MEMLIMIT])]
-        if benchexec.model.TIMELIMIT in rlimits:
-            options += ["--max-time=" + str(rlimits[benchexec.model.TIMELIMIT])]
-        if benchexec.model.WALLTIMELIMIT in rlimits:
-            options += ["--max-walltime=" + str(rlimits[benchexec.model.WALLTIMELIMIT])]
-        if benchexec.model.SOFTTIMELIMIT in rlimits:
-            options += [
-                "--max-cputime-soft=" + str(rlimits[benchexec.model.SOFTTIMELIMIT])
-            ]
-        if benchexec.model.HARDTIMELIMIT in rlimits:
-            options += [
-                "--max-cputime-hard=" + str(rlimits[benchexec.model.HARDTIMELIMIT])
-            ]
+    def cmdline(self, executable, options, task, rlimits):
+        if task.property_file:
+            options += ["--property-file=" + task.property_file]
+        if rlimits.memory:
+            options += ["--max-memory=" + str(rlimits.memory)]
+        if rlimits.cputime_hard:
+            options += ["--max-time=" + str(rlimits.cputime_hard)]
+        if rlimits.walltime:
+            options += ["--max-walltime=" + str(rlimits.walltime)]
+        if rlimits.cputime:
+            options += ["--max-cputime-soft=" + str(rlimits.cputime)]
+        if rlimits.cputime_hard:
+            options += ["--max-cputime-hard=" + str(rlimits.cputime_hard)]
 
-        return [executable] + options + tasks
+        data_model_param = get_data_model_from_task(
+            task, {"ILP32": "--32", "LP64": "--64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
+
+        return [executable] + options + list(task.input_files_or_identifier)
 
     def name(self):
         return "KLEE"
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
         """
         Parse the output of the tool and extract the verification result.
         This method always needs to be overridden.
@@ -78,7 +80,7 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
         and should give some indication of the failure reason
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
         """
-        for line in output:
+        for line in run.output:
             if line.startswith("KLEE: ERROR: "):
                 if line.find("ASSERTION FAIL:") != -1:
                     return result.RESULT_FALSE_REACH
@@ -87,7 +89,7 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
                 elif line.find("overflow") != -1:
                     return result.RESULT_FALSE_OVERFLOW
                 else:
-                    return "ERROR ({0})".format(returncode)
+                    return "ERROR ({0})".format(run.exit_code.value)
             if line.startswith("KLEE: done"):
                 return result.RESULT_DONE
         return result.RESULT_UNKNOWN

From d7830c01fa3f545b989cdb9e37399ace97a471ff Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Wed, 28 Oct 2020 09:12:18 +0100
Subject: [PATCH 36/46] updated TI for legion, libkluzzer, and prtest

---
 benchexec/tools/legion.py     | 17 +++++++++++++----
 benchexec/tools/libkluzzer.py | 17 +++++++++++++----
 benchexec/tools/prtest.py     | 17 +++++++++++++----
 3 files changed, 39 insertions(+), 12 deletions(-)

diff --git a/benchexec/tools/legion.py b/benchexec/tools/legion.py
index 5ef6f6536..3791b9356 100644
--- a/benchexec/tools/legion.py
+++ b/benchexec/tools/legion.py
@@ -5,11 +5,11 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
 import benchexec.tools.template
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for Legion (https://github.com/Alan32Liu/Legion).
     """
@@ -27,11 +27,20 @@ class Tool(benchexec.tools.template.BaseTool):
         "lib",
     ]
 
-    def executable(self):
-        return util.find_executable("legion-sv")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("legion-sv")
 
     def version(self, executable):
         return self._version_from_tool(executable, ignore_stderr=False)
 
     def name(self):
         return "Legion"
+
+    def cmdline(self, executable, options, task, rlimits):
+        data_model_param = get_data_model_from_task(
+            task, {"ILP32": "-32", "LP64": "-64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
+
+        return super().cmdline(executable, options, task, rlimits)
diff --git a/benchexec/tools/libkluzzer.py b/benchexec/tools/libkluzzer.py
index 58d58a88c..93c88a1c3 100644
--- a/benchexec/tools/libkluzzer.py
+++ b/benchexec/tools/libkluzzer.py
@@ -5,11 +5,11 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
 import benchexec.tools.template
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for LibKluzzer (http://unihb.eu/kluzzer).
     """
@@ -21,11 +21,20 @@ def program_files(self, executable):
             executable, self.REQUIRED_PATHS, parent_dir=True
         )
 
-    def executable(self):
-        return util.find_executable("LibKluzzer", "bin/LibKluzzer")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("LibKluzzer", subdir="bin")
 
     def version(self, executable):
         return self._version_from_tool(executable)
 
     def name(self):
         return "LibKluzzer"
+
+    def cmdline(self, executable, options, task, rlimits):
+        data_model_param = get_data_model_from_task(
+            task, {"ILP32": "--32", "LP64": "--64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
+
+        return super().cmdline(executable, options, task, rlimits)
diff --git a/benchexec/tools/prtest.py b/benchexec/tools/prtest.py
index ec22cdde9..95e3de2db 100644
--- a/benchexec/tools/prtest.py
+++ b/benchexec/tools/prtest.py
@@ -5,11 +5,11 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-import benchexec.util as util
 import benchexec.tools.template
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for PRTest (https://gitlab.com/sosy-lab/software/prtest).
     """
@@ -21,11 +21,20 @@ def program_files(self, executable):
             executable, self.REQUIRED_PATHS, parent_dir=True
         )
 
-    def executable(self):
-        return util.find_executable("prtest", "bin/prtest")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("prtest", subdir="bin")
 
     def version(self, executable):
         return self._version_from_tool(executable)
 
     def name(self):
         return "PRTest"
+
+    def cmdline(self, executable, options, task, rlimits):
+        data_model_param = get_data_model_from_task(
+            task, {"ILP32": "-m32", "LP64": "-m64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
+
+        return super().cmdline(executable, options, task, rlimits)

From f687090ad50d47e2e33d26b84e1c645fcc9bccd2 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Wed, 28 Oct 2020 09:17:08 +0100
Subject: [PATCH 37/46] updated TI for tracerx

---
 benchexec/tools/tracerx.py | 52 ++++++++++++++++++++------------------
 1 file changed, 27 insertions(+), 25 deletions(-)

diff --git a/benchexec/tools/tracerx.py b/benchexec/tools/tracerx.py
index 257bc1fc2..30a7d9214 100644
--- a/benchexec/tools/tracerx.py
+++ b/benchexec/tools/tracerx.py
@@ -6,12 +6,12 @@
 # SPDX-License-Identifier: Apache-2.0
 
 import benchexec.result as result
-import benchexec.util as util
 import benchexec.tools.template
 import benchexec.model
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 
 
-class Tool(benchexec.tools.template.BaseTool):
+class Tool(benchexec.tools.template.BaseTool2):
     """
     Tool info for Tracer-X (https://www.comp.nus.edu.sg/~tracerx/).
     """
@@ -24,8 +24,8 @@ class Tool(benchexec.tools.template.BaseTool):
         "tracerx_build",
     ]
 
-    def executable(self):
-        return util.find_executable("bin/tracerx")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("tracerx", subdir="bin")
 
     def program_files(self, executable):
         return self._program_files_from_executable(
@@ -49,30 +49,32 @@ def version(self, executable):
         version = self._version_from_tool(executable, line_prefix="KLEE")
         return version.split("(")[0].strip()
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
-        if propertyfile:
-            options += ["--property-file=" + propertyfile]
-        if benchexec.model.MEMLIMIT in rlimits:
-            options += ["--max-memory=" + str(rlimits[benchexec.model.MEMLIMIT])]
-        if benchexec.model.TIMELIMIT in rlimits:
-            options += ["--max-time=" + str(rlimits[benchexec.model.TIMELIMIT])]
-        if benchexec.model.WALLTIMELIMIT in rlimits:
-            options += ["--max-walltime=" + str(rlimits[benchexec.model.WALLTIMELIMIT])]
-        if benchexec.model.SOFTTIMELIMIT in rlimits:
-            options += [
-                "--max-cputime-soft=" + str(rlimits[benchexec.model.SOFTTIMELIMIT])
-            ]
-        if benchexec.model.HARDTIMELIMIT in rlimits:
-            options += [
-                "--max-cputime-hard=" + str(rlimits[benchexec.model.HARDTIMELIMIT])
-            ]
+    def cmdline(self, executable, options, task, rlimits):
+        if task.property_file:
+            options += ["--property-file=" + task.property_file]
+        if rlimits.memory:
+            options += ["--max-memory=" + str(rlimits.memory)]
+        if rlimits.cputime_hard:
+            options += ["--max-time=" + str(rlimits.cputime_hard)]
+        if rlimits.walltime:
+            options += ["--max-walltime=" + str(rlimits.walltime)]
+        if rlimits.cputime:
+            options += ["--max-cputime-soft=" + str(rlimits.cputime)]
+        if rlimits.cputime_hard:
+            options += ["--max-cputime-hard=" + str(rlimits.cputime_hard)]
 
-        return [executable] + options + tasks
+        data_model_param = get_data_model_from_task(
+            task, {"ILP32": "--32", "LP64": "--64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
+
+        return [executable] + options + list(task.input_files_or_identifier)
 
     def name(self):
         return "Tracer-X"
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
         """
         Parse the output of the tool and extract the verification result.
         This method always needs to be overridden.
@@ -82,7 +84,7 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
         and should give some indication of the failure reason
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
         """
-        for line in output:
+        for line in run.output:
             if line.startswith("KLEE: ERROR: "):
                 if "ASSERTION FAIL:" in line:
                     return result.RESULT_FALSE_REACH
@@ -91,7 +93,7 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
                 elif "overflow" in line:
                     return result.RESULT_FALSE_OVERFLOW
                 else:
-                    return "ERROR ({0})".format(returncode)
+                    return "ERROR ({0})".format(run.exit_code.value)
             if line.startswith("KLEE: done"):
                 return result.RESULT_DONE
         return result.RESULT_UNKNOWN

From e562c6113eb2ef7e4d45133b1c08c3c0d3299d86 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Wed, 28 Oct 2020 09:23:09 +0100
Subject: [PATCH 38/46] updated TI for testcov

---
 benchexec/tools/testcov.py | 26 ++++++++++++++++----------
 1 file changed, 16 insertions(+), 10 deletions(-)

diff --git a/benchexec/tools/testcov.py b/benchexec/tools/testcov.py
index 0185d0586..bab3061d1 100644
--- a/benchexec/tools/testcov.py
+++ b/benchexec/tools/testcov.py
@@ -7,8 +7,8 @@
 
 import re
 import benchexec.result as result
-import benchexec.util as util
 import benchexec.tools.template
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
 
 
 class Tool(benchexec.tools.template.BaseTool):
@@ -23,15 +23,21 @@ def program_files(self, executable):
             executable, self.REQUIRED_PATHS, parent_dir=True
         )
 
-    def executable(self):
-        return util.find_executable("testcov", "bin/testcov")
+    def executable(self, tool_locator):
+        return tool_locator.find_executable("testcov", subdir="bin")
+
+    def cmdline(self, executable, options, task, rlimits):
+        data_model_param = get_data_model_from_task(
+            task, {"ILP32": "-32", "LP64": "-64"}
+        )
+        if data_model_param and data_model_param not in options:
+            options += [data_model_param]
 
-    def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
         cmd = [executable] + options
-        if propertyfile:
-            cmd += ["--goal", propertyfile]
+        if task.property_file:
+            cmd += ["--goal", task.property_file]
 
-        return cmd + tasks
+        return cmd + list(task.input_files_or_identifier)
 
     def version(self, executable):
         return self._version_from_tool(executable)
@@ -39,7 +45,7 @@ def version(self, executable):
     def name(self):
         return "TestCov"
 
-    def determine_result(self, returncode, returnsignal, output, isTimeout):
+    def determine_result(self, run):
         """
         Parse the output of the tool and extract the verification result.
         This method always needs to be overridden.
@@ -49,12 +55,12 @@ def determine_result(self, returncode, returnsignal, output, isTimeout):
         and should give some indication of the failure reason
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
         """
-        for line in reversed(output):
+        for line in reversed(run.output):
             if line.startswith("ERROR:"):
                 if "timeout" in line.lower():
                     return "TIMEOUT"
                 else:
-                    return "ERROR ({0})".format(returncode)
+                    return "ERROR ({0})".format(run.exit_code.value)
             elif line.startswith("Result: FALSE"):
                 return result.RESULT_FALSE_REACH
             elif line.startswith("Result: TRUE"):

From 6f11a4cb9c66b01effc2b0a591ce95e368f99631 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Wed, 28 Oct 2020 12:52:00 +0100
Subject: [PATCH 39/46] doc for the function get_data_model_from_task

---
 benchexec/tools/sv_benchmarks_util.py | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/benchexec/tools/sv_benchmarks_util.py b/benchexec/tools/sv_benchmarks_util.py
index c5ca1574c..82ab866ba 100644
--- a/benchexec/tools/sv_benchmarks_util.py
+++ b/benchexec/tools/sv_benchmarks_util.py
@@ -8,16 +8,28 @@
 """
 This module contains some useful functions related to tasks in the sv-benchmarks
 repository: https://github.com/sosy-lab/sv-benchmarks
+
+Note the following points before using any function in this util:
+    1. This is not a part of stable benchexec API.
+       We do not provide any guarantee of backward compatibility of this module.
+    2. Out-of-tree modules should not use this util
+    3. Any function in this util may change at any point in time
 """
 
 import benchexec.tools.template
 
 
-def get_data_model_from_task(task, data_models):
+def get_data_model_from_task(task, param_dict):
+    """
+    This function tries to extract tool parameter for data model
+    depending on the data model in the task.
+    @param task: An instance of of class Task, e.g., with the input files
+    @param param_dict: Dictionary mapping data model to the tool param value
+    """
     if isinstance(task.options, dict) and task.options.get("language") == "C":
         data_model = task.options.get("data_model")
         if data_model:
-            data_model_option = data_models.get(data_model)
+            data_model_option = param_dict.get(data_model)
             if data_model_option:
                 return data_model_option
             else:

From a6dbfcbc3fefc99d6a7a99e9a4040b7dee88e614 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Thu, 29 Oct 2020 16:47:01 +0100
Subject: [PATCH 40/46] updated cbmc TI

---
 benchexec/tools/cbmc.py | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/benchexec/tools/cbmc.py b/benchexec/tools/cbmc.py
index 55fae1544..8500cc6a8 100644
--- a/benchexec/tools/cbmc.py
+++ b/benchexec/tools/cbmc.py
@@ -114,7 +114,7 @@ def determine_result(self, run):
         if run.exit_code.value in [0, 10]:
             status = result.RESULT_ERROR
             if "--xml-ui" in self.options:
-                status = self.parse_XML(output, run.exit_code.value, run.was_timeout)
+                status = self.parse_XML(output, run.exit_code, run.was_timeout)
             elif len(output) > 0:
                 # SV-COMP mode
                 result_str = output[-1].strip()
@@ -137,13 +137,13 @@ def determine_result(self, run):
                 elif "UNKNOWN" in output:
                     status = result.RESULT_UNKNOWN
 
-        elif run.exit_code.value == 64 and "Usage error!\n" in output:
+        elif run.exit_code.value == 64 and "Usage error!" in output:
             status = "INVALID ARGUMENTS"
 
-        elif run.exit_code.value == 6 and "Out of memory\n" in output:
+        elif run.exit_code.value == 6 and "Out of memory" in output:
             status = "OUT OF MEMORY"
 
-        elif run.exit_code.value == 6 and "SAT checker ran out of memory\n" in output:
+        elif run.exit_code.value == 6 and "SAT checker ran out of memory" in output:
             status = "OUT OF MEMORY"
 
         else:

From 53d68f15f868f1dca4a307f032076a0ddc5a43c3 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Thu, 29 Oct 2020 16:47:18 +0100
Subject: [PATCH 41/46] updated divine based TIs

---
 benchexec/tools/divine.py  | 6 ++----
 benchexec/tools/divine4.py | 2 --
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/benchexec/tools/divine.py b/benchexec/tools/divine.py
index 330766a2a..d7df6f78c 100644
--- a/benchexec/tools/divine.py
+++ b/benchexec/tools/divine.py
@@ -104,12 +104,10 @@ def determine_result(self, run):
         if run.was_timeout:
             return "TIMEOUT"
 
-        if run.exit_code.value != 0:
+        if run.exit_code.value and run.exit_code.value != 0:
             return "ERROR - Pre-run"
 
-        if last is None:
-            return "ERROR - no output"
-        elif "result: true" in last:
+        if "result: true" in last:
             return result.RESULT_TRUE_PROP
         elif "result: false" in last:
             return result.RESULT_FALSE_REACH
diff --git a/benchexec/tools/divine4.py b/benchexec/tools/divine4.py
index 34df27a8e..cf35e3b29 100644
--- a/benchexec/tools/divine4.py
+++ b/benchexec/tools/divine4.py
@@ -94,8 +94,6 @@ def determine_result(self, run):
         and should give some indication of the failure reason
         (e.g., "CRASH", "OUT_OF_MEMORY", etc.).
         """
-        run.exit_code.value = run.exit_code.value or 0
-
         if not run.output:
             return "ERROR - no output"
 

From 4b7464cc40a620880e02a86218a0eb1d0b26ac8c Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Thu, 29 Oct 2020 16:50:44 +0100
Subject: [PATCH 42/46] removed super call in cmdline from legion, libkluzzer
 and prtest

---
 benchexec/tools/legion.py     | 2 +-
 benchexec/tools/libkluzzer.py | 2 +-
 benchexec/tools/prtest.py     | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/benchexec/tools/legion.py b/benchexec/tools/legion.py
index 3791b9356..3d186ca5f 100644
--- a/benchexec/tools/legion.py
+++ b/benchexec/tools/legion.py
@@ -43,4 +43,4 @@ def cmdline(self, executable, options, task, rlimits):
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
-        return super().cmdline(executable, options, task, rlimits)
+        return [executable, *options, *task.input_files_or_identifier]
diff --git a/benchexec/tools/libkluzzer.py b/benchexec/tools/libkluzzer.py
index 93c88a1c3..8659a22d9 100644
--- a/benchexec/tools/libkluzzer.py
+++ b/benchexec/tools/libkluzzer.py
@@ -37,4 +37,4 @@ def cmdline(self, executable, options, task, rlimits):
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
-        return super().cmdline(executable, options, task, rlimits)
+        return [executable, *options, *task.input_files_or_identifier]
diff --git a/benchexec/tools/prtest.py b/benchexec/tools/prtest.py
index 95e3de2db..65cd64de2 100644
--- a/benchexec/tools/prtest.py
+++ b/benchexec/tools/prtest.py
@@ -37,4 +37,4 @@ def cmdline(self, executable, options, task, rlimits):
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
-        return super().cmdline(executable, options, task, rlimits)
+        return [executable, *options, *task.input_files_or_identifier]

From dfb784c34463564e65652465cd7bdde773d1d174 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Thu, 29 Oct 2020 16:57:58 +0100
Subject: [PATCH 43/46] updated pinaka TI

---
 benchexec/tools/pinaka.py | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/benchexec/tools/pinaka.py b/benchexec/tools/pinaka.py
index 7bdf424cc..08f6e679e 100644
--- a/benchexec/tools/pinaka.py
+++ b/benchexec/tools/pinaka.py
@@ -38,11 +38,11 @@ def determine_result(self, run):
         status = ""
 
         if run.exit_code.value in [0, 10]:
-            if run.output.any_line_contains("VERIFICATION FAILED (ReachSafety)"):
+            if "VERIFICATION FAILED (ReachSafety)" in run.output:
                 status = result.RESULT_FALSE_REACH
-            elif run.output.any_line_contains("VERIFICATION FAILED (NoOverflow)"):
+            elif "VERIFICATION FAILED (NoOverflow)" in run.output:
                 status = result.RESULT_FALSE_OVERFLOW
-            elif run.output.any_line_contains("VERIFICATION SUCCESSFUL"):
+            elif "VERIFICATION SUCCESSFUL" in run.output:
                 status = result.RESULT_TRUE_PROP
             else:
                 status = result.RESULT_UNKNOWN

From 59886567a1e060133a94b09ebc336b10a5336361 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Thu, 29 Oct 2020 22:04:00 +0100
Subject: [PATCH 44/46] updated divine TI

---
 benchexec/tools/divine4.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/benchexec/tools/divine4.py b/benchexec/tools/divine4.py
index cf35e3b29..45327f920 100644
--- a/benchexec/tools/divine4.py
+++ b/benchexec/tools/divine4.py
@@ -102,7 +102,7 @@ def determine_result(self, run):
         if run.was_timeout:
             return "TIMEOUT"
 
-        if run.exit_code.value != 0:
+        if run.exit_code.value and run.exit_code.value != 0:
             return "ERROR - {0}".format(last)
 
         if "result:" in last:

From aaeae7166b8469eebf828b91ee9f6fe768e1afc7 Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Fri, 30 Oct 2020 12:13:36 +0100
Subject: [PATCH 45/46] updated klee and tracerx TI modules: using only
 rlimits.cputime

---
 benchexec/tools/klee.py    | 6 ------
 benchexec/tools/tracerx.py | 6 ------
 2 files changed, 12 deletions(-)

diff --git a/benchexec/tools/klee.py b/benchexec/tools/klee.py
index 460bd8d4c..1b0ec3b46 100644
--- a/benchexec/tools/klee.py
+++ b/benchexec/tools/klee.py
@@ -50,14 +50,8 @@ def cmdline(self, executable, options, task, rlimits):
             options += ["--property-file=" + task.property_file]
         if rlimits.memory:
             options += ["--max-memory=" + str(rlimits.memory)]
-        if rlimits.cputime_hard:
-            options += ["--max-time=" + str(rlimits.cputime_hard)]
-        if rlimits.walltime:
-            options += ["--max-walltime=" + str(rlimits.walltime)]
         if rlimits.cputime:
             options += ["--max-cputime-soft=" + str(rlimits.cputime)]
-        if rlimits.cputime_hard:
-            options += ["--max-cputime-hard=" + str(rlimits.cputime_hard)]
 
         data_model_param = get_data_model_from_task(
             task, {"ILP32": "--32", "LP64": "--64"}
diff --git a/benchexec/tools/tracerx.py b/benchexec/tools/tracerx.py
index 30a7d9214..33537a14e 100644
--- a/benchexec/tools/tracerx.py
+++ b/benchexec/tools/tracerx.py
@@ -54,14 +54,8 @@ def cmdline(self, executable, options, task, rlimits):
             options += ["--property-file=" + task.property_file]
         if rlimits.memory:
             options += ["--max-memory=" + str(rlimits.memory)]
-        if rlimits.cputime_hard:
-            options += ["--max-time=" + str(rlimits.cputime_hard)]
-        if rlimits.walltime:
-            options += ["--max-walltime=" + str(rlimits.walltime)]
         if rlimits.cputime:
             options += ["--max-cputime-soft=" + str(rlimits.cputime)]
-        if rlimits.cputime_hard:
-            options += ["--max-cputime-hard=" + str(rlimits.cputime_hard)]
 
         data_model_param = get_data_model_from_task(
             task, {"ILP32": "--32", "LP64": "--64"}

From 34427e77194d38ad7fd29360d1df63687f8fd6be Mon Sep 17 00:00:00 2001
From: Sudeep Kanav <sudeep.kanav@lmu.de>
Date: Fri, 30 Oct 2020 18:52:25 +0100
Subject: [PATCH 46/46] introduced constants for ILP32 and LP64

---
 benchexec/tools/brick.py               | 6 ++----
 benchexec/tools/cbmc.py                | 6 ++----
 benchexec/tools/divine.py              | 6 ++----
 benchexec/tools/divine4.py             | 6 ++----
 benchexec/tools/esbmc.py               | 4 ++--
 benchexec/tools/fshell-witness2test.py | 6 ++----
 benchexec/tools/gacal.py               | 4 ++--
 benchexec/tools/klee.py                | 6 ++----
 benchexec/tools/legion.py              | 6 ++----
 benchexec/tools/libkluzzer.py          | 6 ++----
 benchexec/tools/pinaka.py              | 6 ++----
 benchexec/tools/predatorhp.py          | 4 ++--
 benchexec/tools/prtest.py              | 6 ++----
 benchexec/tools/sv_benchmarks_util.py  | 4 ++++
 benchexec/tools/symbiotic4.py          | 6 ++----
 benchexec/tools/testcov.py             | 6 ++----
 benchexec/tools/tracerx.py             | 6 ++----
 benchexec/tools/two_ls.py              | 6 ++----
 benchexec/tools/verifuzz.py            | 4 ++--
 19 files changed, 40 insertions(+), 64 deletions(-)

diff --git a/benchexec/tools/brick.py b/benchexec/tools/brick.py
index b64713ad3..a93b3055c 100644
--- a/benchexec/tools/brick.py
+++ b/benchexec/tools/brick.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -25,9 +25,7 @@ def name(self):
         return "BRICK"
 
     def cmdline(self, executable, options, task, rlimits):
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "--32", "LP64": "--64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "--32", LP64: "--64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/cbmc.py b/benchexec/tools/cbmc.py
index 8500cc6a8..40acb1cb8 100644
--- a/benchexec/tools/cbmc.py
+++ b/benchexec/tools/cbmc.py
@@ -8,7 +8,7 @@
 import logging
 from xml.etree import ElementTree
 
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -38,9 +38,7 @@ def cmdline(self, executable, options, task, rlimits):
         elif "--xml-ui" not in options:
             options = options + ["--xml-ui"]
 
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "--32", "LP64": "--64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "--32", LP64: "--64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/divine.py b/benchexec/tools/divine.py
index d7df6f78c..36c31278c 100644
--- a/benchexec/tools/divine.py
+++ b/benchexec/tools/divine.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -70,9 +70,7 @@ def cmdline(self, executable, options, task, rlimits):
                         for example: time-limit, soft-time-limit, hard-time-limit, memory-limit, cpu-core-limit.
                         All entries in rlimits are optional, so check for existence before usage!
         """
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "--32", "LP64": "--64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "--32", LP64: "--64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/divine4.py b/benchexec/tools/divine4.py
index 45327f920..43439cb87 100644
--- a/benchexec/tools/divine4.py
+++ b/benchexec/tools/divine4.py
@@ -6,7 +6,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -68,9 +68,7 @@ def cmdline(self, executable, options, task, rlimits):
                         for example: time-limit, soft-time-limit, hard-time-limit, memory-limit, cpu-core-limit.
                         All entries in rlimits are optional, so check for existence before usage!
         """
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "--32", "LP64": "--64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "--32", LP64: "--64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/esbmc.py b/benchexec/tools/esbmc.py
index 42482f519..f636209a4 100644
--- a/benchexec/tools/esbmc.py
+++ b/benchexec/tools/esbmc.py
@@ -6,7 +6,7 @@
 # SPDX-License-Identifier: Apache-2.0
 
 import os
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -32,7 +32,7 @@ def name(self):
         return "ESBMC"
 
     def cmdline(self, executable, options, task, rlimits):
-        data_model_param = get_data_model_from_task(task, {"ILP32": "32", "LP64": "64"})
+        data_model_param = get_data_model_from_task(task, {ILP32: "32", LP64: "64"})
         if data_model_param and "--arch" not in options:
             options += ["--arch", data_model_param]
         return (
diff --git a/benchexec/tools/fshell-witness2test.py b/benchexec/tools/fshell-witness2test.py
index 24c7a0fa7..1082cead5 100644
--- a/benchexec/tools/fshell-witness2test.py
+++ b/benchexec/tools/fshell-witness2test.py
@@ -9,7 +9,7 @@
 
 import benchexec.result as result
 import benchexec.tools.template
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 
 
 class Tool(benchexec.tools.template.BaseTool2):
@@ -63,9 +63,7 @@ def cmdline(self, executable, options, task, rlimits):
         if task.property_file:
             options = options + ["--propertyfile", task.property_file]
 
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "-m32", "LP64": "-m64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "-m32", LP64: "-m64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/gacal.py b/benchexec/tools/gacal.py
index 65c736f10..fda792ba8 100644
--- a/benchexec/tools/gacal.py
+++ b/benchexec/tools/gacal.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -35,7 +35,7 @@ def version(self, executable):
         return self._version_from_tool(executable)
 
     def cmdline(self, executable, options, task, rlimits):
-        data_model_param = get_data_model_from_task(task, {"ILP32": "32", "LP64": "64"})
+        data_model_param = get_data_model_from_task(task, {ILP32: "32", LP64: "64"})
         if data_model_param and "--architecture" not in options:
             options += ["--architecture", data_model_param]
 
diff --git a/benchexec/tools/klee.py b/benchexec/tools/klee.py
index 1b0ec3b46..4097ffd14 100644
--- a/benchexec/tools/klee.py
+++ b/benchexec/tools/klee.py
@@ -8,7 +8,7 @@
 import benchexec.result as result
 import benchexec.tools.template
 import benchexec.model
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 
 
 class Tool(benchexec.tools.template.BaseTool2):
@@ -53,9 +53,7 @@ def cmdline(self, executable, options, task, rlimits):
         if rlimits.cputime:
             options += ["--max-cputime-soft=" + str(rlimits.cputime)]
 
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "--32", "LP64": "--64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "--32", LP64: "--64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/legion.py b/benchexec/tools/legion.py
index 3d186ca5f..2403d708d 100644
--- a/benchexec/tools/legion.py
+++ b/benchexec/tools/legion.py
@@ -6,7 +6,7 @@
 # SPDX-License-Identifier: Apache-2.0
 
 import benchexec.tools.template
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 
 
 class Tool(benchexec.tools.template.BaseTool2):
@@ -37,9 +37,7 @@ def name(self):
         return "Legion"
 
     def cmdline(self, executable, options, task, rlimits):
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "-32", "LP64": "-64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "-32", LP64: "-64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/libkluzzer.py b/benchexec/tools/libkluzzer.py
index 8659a22d9..bc40feaf3 100644
--- a/benchexec/tools/libkluzzer.py
+++ b/benchexec/tools/libkluzzer.py
@@ -6,7 +6,7 @@
 # SPDX-License-Identifier: Apache-2.0
 
 import benchexec.tools.template
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 
 
 class Tool(benchexec.tools.template.BaseTool2):
@@ -31,9 +31,7 @@ def name(self):
         return "LibKluzzer"
 
     def cmdline(self, executable, options, task, rlimits):
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "--32", "LP64": "--64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "--32", LP64: "--64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/pinaka.py b/benchexec/tools/pinaka.py
index 08f6e679e..6d0f68991 100644
--- a/benchexec/tools/pinaka.py
+++ b/benchexec/tools/pinaka.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -26,9 +26,7 @@ def name(self):
     def cmdline(self, executable, options, task, rlimits):
         if task.property_file:
             options = options + ["--propertyfile", task.property_file]
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "--32", "LP64": "--64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "--32", LP64: "--64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/predatorhp.py b/benchexec/tools/predatorhp.py
index 4910790b0..c89b23025 100644
--- a/benchexec/tools/predatorhp.py
+++ b/benchexec/tools/predatorhp.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -32,7 +32,7 @@ def cmdline(self, executable, options, task, rlimits):
 
         data_model_param = get_data_model_from_task(
             task,
-            {"ILP32": "--compiler-options=-m32", "LP64": "--compiler-options=-m64"},
+            {ILP32: "--compiler-options=-m32", LP64: "--compiler-options=-m64"},
         )
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
diff --git a/benchexec/tools/prtest.py b/benchexec/tools/prtest.py
index 65cd64de2..f0c276691 100644
--- a/benchexec/tools/prtest.py
+++ b/benchexec/tools/prtest.py
@@ -6,7 +6,7 @@
 # SPDX-License-Identifier: Apache-2.0
 
 import benchexec.tools.template
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 
 
 class Tool(benchexec.tools.template.BaseTool2):
@@ -31,9 +31,7 @@ def name(self):
         return "PRTest"
 
     def cmdline(self, executable, options, task, rlimits):
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "-m32", "LP64": "-m64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "-m32", LP64: "-m64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/sv_benchmarks_util.py b/benchexec/tools/sv_benchmarks_util.py
index 82ab866ba..c77d8e0ab 100644
--- a/benchexec/tools/sv_benchmarks_util.py
+++ b/benchexec/tools/sv_benchmarks_util.py
@@ -18,6 +18,10 @@
 
 import benchexec.tools.template
 
+# Defining constants for data model.
+ILP32 = "ILP32"
+LP64 = "LP64"
+
 
 def get_data_model_from_task(task, param_dict):
     """
diff --git a/benchexec/tools/symbiotic4.py b/benchexec/tools/symbiotic4.py
index ee1109409..6d2ca6736 100644
--- a/benchexec/tools/symbiotic4.py
+++ b/benchexec/tools/symbiotic4.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -54,9 +54,7 @@ def cmdline(self, executable, options, task, rlimits):
         if task.property_file:
             options = options + ["--prp={0}".format(task.property_file)]
 
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "--32", "LP64": "--64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "--32", LP64: "--64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/testcov.py b/benchexec/tools/testcov.py
index bab3061d1..e2d870ed9 100644
--- a/benchexec/tools/testcov.py
+++ b/benchexec/tools/testcov.py
@@ -8,7 +8,7 @@
 import re
 import benchexec.result as result
 import benchexec.tools.template
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 
 
 class Tool(benchexec.tools.template.BaseTool):
@@ -27,9 +27,7 @@ def executable(self, tool_locator):
         return tool_locator.find_executable("testcov", subdir="bin")
 
     def cmdline(self, executable, options, task, rlimits):
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "-32", "LP64": "-64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "-32", LP64: "-64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/tracerx.py b/benchexec/tools/tracerx.py
index 33537a14e..f9436dcaa 100644
--- a/benchexec/tools/tracerx.py
+++ b/benchexec/tools/tracerx.py
@@ -8,7 +8,7 @@
 import benchexec.result as result
 import benchexec.tools.template
 import benchexec.model
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 
 
 class Tool(benchexec.tools.template.BaseTool2):
@@ -57,9 +57,7 @@ def cmdline(self, executable, options, task, rlimits):
         if rlimits.cputime:
             options += ["--max-cputime-soft=" + str(rlimits.cputime)]
 
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "--32", "LP64": "--64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "--32", LP64: "--64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/two_ls.py b/benchexec/tools/two_ls.py
index e6e7cabc8..9232de73d 100644
--- a/benchexec/tools/two_ls.py
+++ b/benchexec/tools/two_ls.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -30,9 +30,7 @@ def cmdline(self, executable, options, task, rlimits):
         if task.property_file:
             options = options + ["--propertyfile", task.property_file]
 
-        data_model_param = get_data_model_from_task(
-            task, {"ILP32": "--32", "LP64": "--64"}
-        )
+        data_model_param = get_data_model_from_task(task, {ILP32: "--32", LP64: "--64"})
         if data_model_param and data_model_param not in options:
             options += [data_model_param]
 
diff --git a/benchexec/tools/verifuzz.py b/benchexec/tools/verifuzz.py
index 9a7822142..ea745499e 100644
--- a/benchexec/tools/verifuzz.py
+++ b/benchexec/tools/verifuzz.py
@@ -5,7 +5,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-from benchexec.tools.sv_benchmarks_util import get_data_model_from_task
+from benchexec.tools.sv_benchmarks_util import get_data_model_from_task, ILP32, LP64
 import benchexec.tools.template
 import benchexec.result as result
 
@@ -45,7 +45,7 @@ def cmdline(self, executable, options, task, rlimits):
         if task.property_file:
             options = options + ["--propertyFile", task.property_file]
 
-        data_model_param = get_data_model_from_task(task, {"ILP32": "32", "LP64": "64"})
+        data_model_param = get_data_model_from_task(task, {ILP32: "32", LP64: "64"})
         if data_model_param and "--bit" not in options:
             options += ["--bit", data_model_param]