From f0ec3dd6a2e8626426cc8c7143713c4a18fd880b Mon Sep 17 00:00:00 2001 From: Simon Tian <9939278+simontianx@users.noreply.github.com> Date: Tue, 6 Jul 2021 23:24:37 +0800 Subject: [PATCH] Update smtchecker.rst --- docs/smtchecker.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index 6fc0a1c57..dff8c8463 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -15,7 +15,7 @@ difference between what you did (the specification) and how you did it is what you wanted and that you did not miss any unintended effects of it. Solidity implements a formal verification approach based on -`SMT `_ and +`SMT (Satisfiability Modulo Theories) `_ and `Horn `_ solving. The SMTChecker module automatically tries to prove that the code satisfies the specification given by ``require`` and ``assert`` statements. That is, it considers