-+-----------------+---------------------------------------------------------+
-| Option | Description |
-+=================+=========================================================+
-| ``--nomem`` | Don't use the SMT theory of arrays to model memories. |
-| | Instead synthesize memories to registers and address |
-| | logic. |
-+-----------------+---------------------------------------------------------+
-| ``--syn`` | Synthesize the circuit to a gate-level representation |
-| | instead of using word-level SMT operators. This also |
-| | runs some low-level logic optimization on the circuit. |
-+-----------------+---------------------------------------------------------+
-| ``--stbv`` | Use large bit vectors (instead of uninterpreted |
-| | functions) to represent the circuit state. |
-+-----------------+---------------------------------------------------------+
-| ``--stdt`` | Use SMT-LIB 2.6 datatypes to represent states. |
-+-----------------+---------------------------------------------------------+
-| ``--nopresat`` | Do not run "presat" SMT queries that make sure that |
-| | assumptions are non-conflicting (and potentially |
-| | warmup the SMT solver). |
-+-----------------+---------------------------------------------------------+
-| ``--unroll``, | Disable/enable unrolling of the SMT problem. The |
-| ``--nounroll`` | default value depends on the solver being used. |
-+-----------------+---------------------------------------------------------+
-| ``--dumpsmt2`` | Write the SMT2 trace to an additional output file. |
-| | (Useful for benchmarking and troubleshooting.) |
-+-----------------+---------------------------------------------------------+
-| ``--progress`` | Enable Yosys-SMTBMC timer display. |
-+-----------------+---------------------------------------------------------+
++------------------+---------------------------------------------------------+
+| Option | Description |
++==================+=========================================================+
+| ``--nomem`` | Don't use the SMT theory of arrays to model memories. |
+| | Instead synthesize memories to registers and address |
+| | logic. |
++------------------+---------------------------------------------------------+
+| ``--syn`` | Synthesize the circuit to a gate-level representation |
+| | instead of using word-level SMT operators. This also |
+| | runs some low-level logic optimization on the circuit. |
++------------------+---------------------------------------------------------+
+| ``--stbv`` | Use large bit vectors (instead of uninterpreted |
+| | functions) to represent the circuit state. |
++------------------+---------------------------------------------------------+
+| ``--stdt`` | Use SMT-LIB 2.6 datatypes to represent states. |
++------------------+---------------------------------------------------------+
+| ``--nopresat`` | Do not run "presat" SMT queries that make sure that |
+| | assumptions are non-conflicting (and potentially |
+| | warmup the SMT solver). |
++------------------+---------------------------------------------------------+
+| ``--keep-going`` | In BMC mode, continue after the first failed assertion |
+| | and report further failed assertions. |
++------------------+---------------------------------------------------------+
+| ``--unroll``, | Disable/enable unrolling of the SMT problem. The |
+| ``--nounroll`` | default value depends on the solver being used. |
++------------------+---------------------------------------------------------+
+| ``--dumpsmt2`` | Write the SMT2 trace to an additional output file. |
+| | (Useful for benchmarking and troubleshooting.) |
++------------------+---------------------------------------------------------+
+| ``--progress`` | Enable Yosys-SMTBMC timer display. |
++------------------+---------------------------------------------------------+