From 5a04ac3fccc91b86e8b66e7fab31ff5c261e1c51 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Wed, 12 Jan 2022 10:48:32 +0100 Subject: [PATCH] use --witness option when calling pono --- sbysrc/sby_engine_btor.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 15344d8..bf9216b 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -46,7 +46,7 @@ def run(mode, task, engine_idx, engine): elif solver_args[0] == "pono": if random_seed: task.error("Setting the random seed is not available for the pono solver.") - solver_cmd = task.exe_paths["pono"] + f" -v 1 -e bmc -k {task.opt_depth - 1}" + solver_cmd = task.exe_paths["pono"] + f" --witness -v 1 -e bmc -k {task.opt_depth - 1}" else: task.error(f"Invalid solver command {solver_args[0]}.") -- 2.30.2