diff --git a/docs/examples/demos/up_down_counter.sby b/docs/examples/demos/up_down_counter.sby
index cb922eb3..4ad57349 100644
--- a/docs/examples/demos/up_down_counter.sby
+++ b/docs/examples/demos/up_down_counter.sby
@@ -1,6 +1,7 @@
 [tasks]
 suprove
 avy
+rIC3
 
 [options]
 mode prove
@@ -8,6 +9,7 @@ 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 ba578d20..ddd8eb57 100644
--- a/docs/source/install.rst
+++ b/docs/source/install.rst
@@ -133,3 +133,7 @@ super_prove
 Avy
 ^^^
   https://arieg.bitbucket.io/avy/
+
+rIC3
+^^^^
+  https://github.com/gipsyh/rIC3/
diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 7b92d7c2..6f9c09ce 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -248,6 +248,8 @@ The following mode/engine/solver combinations are currently supported:
 |           |                          |
 |           | ``aiger avy``            |
 |           |                          |
+|           | ``aiger rIC3``           |
+|           |                          |
 |           | ``aiger suprove``        |
 +-----------+--------------------------+
 | ``cover`` | ``smtbmc [all solvers]`` |
@@ -341,6 +343,8 @@ solvers:
 +-------------------------------+---------------------------------+
 | ``avy``                       |   ``prove``                     |
 +-------------------------------+---------------------------------+
+| ``rIC3``                      |   ``prove``                     |
++-------------------------------+---------------------------------+
 | ``aigbmc``                    |   ``bmc``                       |
 +-------------------------------+---------------------------------+
 
diff --git a/sbysrc/sby_cmdline.py b/sbysrc/sby_cmdline.py
index 2c676daf..812c0c5e 100644
--- a/sbysrc/sby_cmdline.py
+++ b/sbysrc/sby_cmdline.py
@@ -49,6 +49,8 @@ def parser_func(release_version='unknown SBY version'):
             action=DictAction, dest="exe_paths")
     parser.add_argument("--avy", metavar="<path_to_executable>",
             action=DictAction, dest="exe_paths")
+    parser.add_argument("--rIC3", metavar="<path_to_executable>",
+            action=DictAction, dest="exe_paths")
     parser.add_argument("--btormc", metavar="<path_to_executable>",
             action=DictAction, dest="exe_paths")
     parser.add_argument("--pono", metavar="<path_to_executable>",
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index c0444d73..c181c187 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -849,6 +849,7 @@ def __init__(self, sbyconfig, workdir, early_logs, reusedir, taskloop=None, logf
             "suprove": os.getenv("SUPROVE", "suprove"),
             "aigbmc": os.getenv("AIGBMC", "aigbmc"),
             "avy": os.getenv("AVY", "avy"),
+            "rIC3": os.getenv("RIC3", "rIC3"),
             "btormc": os.getenv("BTORMC", "btormc"),
             "pono": os.getenv("PONO", "pono"),
             "imctk-eqy-engine": os.getenv("IMCTK_EQY_ENGINE", "imctk-eqy-engine"),
diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index f18e35d8..d8c78536 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -46,6 +46,11 @@ def run(mode, task, engine_idx, engine):
         if mode != "prove":
             task.error("The aiger solver 'avy' is only supported in prove mode.")
         solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:])
+    
+    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:])
 
     elif solver_args[0] == "aigbmc":
         if mode != "bmc":
@@ -87,7 +92,7 @@ def run(mode, task, engine_idx, engine):
         f"cd {task.workdir}; {solver_cmd} model/design_aiger{model_variant}.aig",
         logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
     )
-    if solver_args[0] not in ["avy"]:
+    if solver_args[0] not in ["avy", "rIC3"]:
         proc.checkretcode = True
 
     proc_status = None