From 34535023f4d3e3d354297cffaf99664aabbeb9bc Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 5 Oct 2026 14:45:42 +0100 Subject: [PATCH 1/2] Document SMT unknown errors Co-authored-by: Codex --- pages/diagnostics/errors.md | 1 + 1 file changed, 1 insertion(+) diff --git a/pages/diagnostics/errors.md b/pages/diagnostics/errors.md index d3e7e4c..a9bd07b 100644 --- a/pages/diagnostics/errors.md +++ b/pages/diagnostics/errors.md @@ -14,6 +14,7 @@ An error can be caused by a refinement violation, an invalid refinement, or anot | --- | --- | | `RefinementError` | A refinement was violated or could not be proven | | `StateRefinementError` | A state refinement was violated or could not be proven | +| `SMTUnknownError` | The solver could not determine whether a refinement holds; the diagnostic includes the reason as a hint | | `NotFoundError` | An element used in a refinement could not be found | | `SyntaxError` | The syntax used in a refinement is invalid | | `ArgumentMismatchError` | A ghost or state invocation has the wrong number or type of arguments | From 0c9ef85d3321dd7a3e5fcfbef5095b026cf64dfb Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 5 Oct 2026 14:49:03 +0100 Subject: [PATCH 2/2] Minor Change --- pages/diagnostics/errors.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pages/diagnostics/errors.md b/pages/diagnostics/errors.md index a9bd07b..e38300e 100644 --- a/pages/diagnostics/errors.md +++ b/pages/diagnostics/errors.md @@ -14,7 +14,7 @@ An error can be caused by a refinement violation, an invalid refinement, or anot | --- | --- | | `RefinementError` | A refinement was violated or could not be proven | | `StateRefinementError` | A state refinement was violated or could not be proven | -| `SMTUnknownError` | The solver could not determine whether a refinement holds; the diagnostic includes the reason as a hint | +| `SMTUnknownError` | The solver could not determine whether a refinement holds | | `NotFoundError` | An element used in a refinement could not be found | | `SyntaxError` | The syntax used in a refinement is invalid | | `ArgumentMismatchError` | A ghost or state invocation has the wrong number or type of arguments |