From f1fdb26ffa012f6cdb8aaebce475f634b34a77db Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Sun, 7 Dec 2025 14:41:56 +0800 Subject: [PATCH] Add support for BTOR rIC3 engine in documentation --- docs/source/reference.rst | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 83629a4..9652f36 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -300,6 +300,8 @@ The following mode/engine/solver combinations are currently supported: | | ``aiger aigbmc`` | | | | | | ``aiger rIC3`` | +| | | +| | ``btor rIC3`` | +-----------+--------------------------+ | ``prove`` | ``smtbmc [all solvers]`` | | | | @@ -307,10 +309,10 @@ The following mode/engine/solver combinations are currently supported: | | | | | ``aiger avy`` | | | | -| | ``aiger rIC3`` | -| | | | | ``aiger suprove`` | | | | +| | ``aiger rIC3`` | +| | | | | ``btor rIC3`` | +-----------+--------------------------+ | ``cover`` | ``smtbmc [all solvers]`` | @@ -387,6 +389,8 @@ The engine supports no engine options and supports the following solvers: +-------------------------------+---------------------------------+ | ``pono`` | ``bmc`` | +-------------------------------+---------------------------------+ +| ``rIC3`` | ``bmc``,``prove`` | ++-------------------------------+---------------------------------+ Solver options are passed to the solver as additional command line options. @@ -404,7 +408,7 @@ solvers: +-------------------------------+---------------------------------+ | ``avy`` | ``prove`` | +-------------------------------+---------------------------------+ -| ``rIC3`` | ``prove`` | +| ``rIC3`` | ``prove``,``bmc`` | +-------------------------------+---------------------------------+ | ``aigbmc`` | ``bmc`` | +-------------------------------+---------------------------------+