diff --git a/benchexec/tools/ultimate.py b/benchexec/tools/ultimate.py index e1a902f2f..1ec69fdbc 100644 --- a/benchexec/tools/ultimate.py +++ b/benchexec/tools/ultimate.py @@ -306,6 +306,7 @@ def _cmdline_no_wrapper(self, executable, options, task, resource_limits): TaskFilesConsidered.INPUT_FILES, ) + cmdline += self._get_task_cmd_options(task, options) cmdline += witness_options cmdline += options @@ -325,6 +326,7 @@ def _cmdline_default(self, executable, options, task): TaskFilesConsidered.INPUT_FILES, ) + cmdline += self._get_task_cmd_options(task, options) cmdline += witness_options if task.input_files_or_empty: cmdline += ["--file", *input_files] @@ -334,9 +336,10 @@ def _cmdline_default(self, executable, options, task): def _cmdline_svcomp17(self, executable, options, task): cmdline = [executable, task.property_file] - cmdline += [ + filtered_options = [ option for option in options if option not in _SVCOMP17_FORBIDDEN_FLAGS ] + cmdline += filtered_options cmdline.append("--full-output") input_files, witness_options = handle_witness_of_task( @@ -346,11 +349,28 @@ def _cmdline_svcomp17(self, executable, options, task): TaskFilesConsidered.INPUT_FILES, ) + cmdline += self._get_task_cmd_options(task, filtered_options) cmdline += witness_options cmdline += input_files self.__assert_cmdline(cmdline, "SVCOMP17") return cmdline + def _get_task_cmd_options(self, task, existing_options): + if not task.options: + return [] + task_options = [] + for plugin, settings in task.options.items(): + if plugin.startswith("de.uni_freiburg.informatik.ultimate."): + prefix = key.split(".")[-1] + for setting, value in settings.items(): + # The same conversion from human-readable setting names to parameters is performed by Ultimate. + name = "--" + (prefix + " " + setting).replace(":", "").sub(r"[ ()\"'.]+", ".").lower().strip(".") + + # Avoid duplicating options (values in benchexec XML take precedence). + if name not in existing_options: + task_options += [name, value] + return task_options + @staticmethod def __assert_cmdline(cmdline, mode): assert all(