rename the instances of smtchecker to solCMC across documentation

Author: furmak331

docs/050-breaking-changes.rst

@@ -152,8 +152,8 @@ Command-line and JSON Interfaces
 
 * The command-line option ``--formal`` (used to generate Why3 output for
   further formal verification) was deprecated and is now removed.  A new
-  formal verification module, the SMTChecker, is enabled via ``pragma
-  experimental SMTChecker;``.
+  formal verification module, the SolCMC, is enabled via ``pragma
+  experimental SolCMC;``.
 
 * The command-line option ``--julia`` was renamed to ``--yul`` due to the
   renaming of the intermediate language ``Julia`` to ``Yul``.

docs/contributing.rst

@@ -140,7 +140,7 @@ However, if ``Eldarica`` is not found, these tests will be automatically skipped
 If ``z3`` is not present on your system, you should disable the
 SMT tests by exporting ``SMT_FLAGS=--no-smt`` before running ``./scripts/tests.sh`` or
 running ``./scripts/soltest.sh --no-smt``.
-These tests are ``libsolidity/smtCheckerTests``.
+These tests are ``libsolidity/solCMCTests``.
 
 .. note::
 

docs/index.rst

@@ -169,7 +169,7 @@ Contents
    :caption: Additional Material
 
    natspec-format.rst
-   smtchecker.rst
+   solcmc.rst
    yul.rst
    path-resolution.rst
 

docs/layout-of-source-files.rst

@@ -147,10 +147,10 @@ Because the ABI coder v2 is not considered experimental anymore,
 it can be selected via ``pragma abicoder v2`` (please see above)
 since Solidity 0.7.4.
 
-.. index:: ! pragma; SMTChecker
-.. _smt_checker:
+.. index:: ! pragma; SolCMC
+.. _solcmc_checker:
 
-SMTChecker
+SolCMC
 ~~~~~~~~~~
 
 This component has to be enabled when the Solidity compiler is built
@@ -162,7 +162,7 @@ statically-built Linux binaries. It can be activated for solc-js via the
 `smtCallback <https://github.com/ethereum/solc-js#example-usage-with-smtsolver-callback>`_ if you have an SMT solver
 installed locally and run solc-js via node (not via the browser).
 
-If you use ``pragma experimental SMTChecker;``, then you get additional
+If you use ``pragma experimental SolCMC;``, then you get additional
 :ref:`safety warnings<formal_verification>` which are obtained by querying an
 SMT solver.
 The component does not yet support all features of the Solidity language and

docs/security-considerations.rst

@@ -318,7 +318,7 @@ In general, read about the limits of two's complement representation, which even
 more special edge cases for signed numbers.
 
 Try to use ``require`` to limit the size of inputs to a reasonable range and use the
-:ref:`SMT checker<smt_checker>` to find potential overflows.
+:ref:`SolCMC<solcmc>` to find potential overflows.
 
 .. _clearing-mappings:
 

docs/smtchecker.rst renamed to docs/solcmc.rst

@@ -490,7 +490,7 @@ Input Description
           "engine": "chc",
           // Choose whether external calls should be considered trusted in case the
           // code of the called function is available at compile-time.
-          // For details see the SMTChecker section.
+          // For details see the SolCMC section.
           "extCalls": "trusted",
           // Choose which types of invariants should be reported to the user: contract, reentrancy.
           "invariants": ["contract", "reentrancy"],
@@ -510,7 +510,7 @@ Input Description
           // See the Formal Verification section for the targets description.
           "targets": ["underflow", "overflow", "assert"],
           // Timeout for each SMT query in milliseconds.
-          // If this option is not given, the SMTChecker will use a deterministic
+          // If this option is not given, the SolCMC will use a deterministic
           // resource limit by default.
           // A given timeout of 0 means no resource/time restrictions for any query.
           "timeout": 20000