From b01f30d763b065839f4e705b265201f17ea5b469 Mon Sep 17 00:00:00 2001 From: inquisitour Date: Fri, 15 May 2026 05:19:58 +0000 Subject: [PATCH] itp engine: add skip and fixpoint justification --- docs/source/reference.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index e08b0fe..4517eec 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -514,7 +514,9 @@ The ``itp`` engine has been verified to produce unbounded safety proofs for the first ``skip`` timeframes, but fixpoint convergence is only guaranteed when ``skip`` is set to 0. Designs requiring non-zero ``skip`` values (e.g. multi-cycle reset sequences) will return bounded - results only. + results only, as pure BMC cannot rule out paths through invalid reset + states without inductive reasoning. This is a property of BMC-based + interpolation, not a limitation specific to this engine. The ``itp`` engine does not currently produce counterexample witness traces. When a property violation is found, only FAIL status is reported.