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":