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