From 141ffd34a5b3f08f3f5395f3c588615550df8bd7 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Tue, 14 Jun 2022 17:56:54 +0200
Subject: [PATCH] btor pono: improve option handling
Fail on the unsupported skip option and pass solver args to pono.
---
sbysrc/sby_engine_btor.py | 3 +++
1 file changed, 3 insertions(+)
diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py
index 7985b32..0fe577b 100644
--- a/sbysrc/sby_engine_btor.py
+++ b/sbysrc/sby_engine_btor.py
@@ -46,7 +46,10 @@ 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.")
+ if task.opt_skip is not None:
+ task.error("The btor engine supports the option skip only for the btormc solver.")
solver_cmd = task.exe_paths["pono"] + f" --witness -v 1 -e bmc -k {task.opt_depth - 1}"
+ solver_cmd += " ".join([""] + solver_args[1:])
else:
task.error(f"Invalid solver command {solver_args[0]}.")