From 3e906f8317bdff1bd48c051e4c4ada8807c70b7f Mon Sep 17 00:00:00 2001
From: Yuheng Su <gipsyh.icu@gmail.com>
Date: Thu, 27 Nov 2025 10:09:53 +0800
Subject: [PATCH] Fix rIC3 BMC command

---
 sbysrc/sby_engine_aiger.py | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index 72add92..3b6c7dc 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -53,7 +53,15 @@ def run(mode, task, engine_idx, engine):
         if mode == "prove":
             solver_cmd = " ".join([task.exe_paths["rIC3"], "--witness"] + solver_args[1:])
         if mode == "bmc":
-            solver_cmd = " ".join([task.exe_paths["rIC3"], "--bmc-max-k {}".format(task.opt_depth - 1), "-e bmc", "-v 0", "--witness"] + solver_args[1:])
+            solver_cmd = " ".join(
+                [
+                    task.exe_paths["rIC3"],
+                    "-e bmc",
+                    "--end {}".format(task.opt_depth - 1),
+                    "--witness",
+                ]
+                + solver_args[1:]
+            )
             status_2 = "PASS"  # rIC3 outputs status 2 when BMC passes
 
     elif solver_args[0] == "aigbmc":