From 8da7174b169b6969fa97b7dbc4e7a359d7cd7aa5 Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Tue, 17 Dec 2024 04:41:58 +0000 Subject: [PATCH] update rIC3 backend Signed-off-by: Yuheng Su --- docs/examples/demos/up_down_counter.sby | 2 -- docs/source/install.rst | 4 ++++ sbysrc/sby_engine_aiger.py | 2 +- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/docs/examples/demos/up_down_counter.sby b/docs/examples/demos/up_down_counter.sby index 4ad5734..cb922eb 100644 --- a/docs/examples/demos/up_down_counter.sby +++ b/docs/examples/demos/up_down_counter.sby @@ -1,7 +1,6 @@ [tasks] suprove avy -rIC3 [options] mode prove @@ -9,7 +8,6 @@ mode prove [engines] suprove: aiger suprove avy: aiger avy -rIC3: aiger rIC3 [script] read_verilog -formal demo.v diff --git a/docs/source/install.rst b/docs/source/install.rst index ddd8eb5..1f9c81a 100644 --- a/docs/source/install.rst +++ b/docs/source/install.rst @@ -137,3 +137,7 @@ Avy rIC3 ^^^^ https://github.com/gipsyh/rIC3/ + +The minimum required version is 1.3.0 + +rIC3 is not allowed to be used for any commercial purposes without authorization. diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index d8c7853..07fc965 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -50,7 +50,7 @@ def run(mode, task, engine_idx, engine): elif solver_args[0] == "rIC3": if mode != "prove": task.error("The aiger solver 'rIC3' is only supported in prove mode.") - solver_cmd = " ".join([task.exe_paths["rIC3"], "-v0", "--sby"] + solver_args[1:]) + solver_cmd = " ".join([task.exe_paths["rIC3"], "--witness"] + solver_args[1:]) elif solver_args[0] == "aigbmc": if mode != "bmc":