From b8e74ffc57370a90f2f2c48316b85cd66a096b2b Mon Sep 17 00:00:00 2001 From: Nuno Santos Date: Thu, 23 Feb 2023 12:09:12 +0000 Subject: [PATCH] Update smtchecker.rst Fixes #13988 --- docs/smtchecker.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index 276f9c33a..05d50cdce 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -706,7 +706,7 @@ Reported Inferred Inductive Invariants For properties that were proved safe with the CHC engine, the SMTChecker can retrieve inductive invariants that were inferred by the Horn solver as part of the proof. -Currently two types of invariants can be reported to the user: +Currently only two types of invariants can be reported to the user: - Contract Invariants: these are properties over the contract's state variables that are true before and after every possible transaction that the contract may ever run. For example, ``x >= y``, where ``x`` and ``y`` are a contract's state variables.