Experimental.md

9 - Experimental

Experimental Pragma: This can be used to enable features of the compiler or language that are not yet enabled by default

1. SMTChecker: The use of pragma experimental SMTChecker; performs additional safety checks which are obtained by querying an SMT solver.

2. The SMTChecker module automatically tries to prove that the code satisfies the specification given by require and assert statements. That is, it considers require statements as assumptions and tries to prove that the conditions inside assert statements are always true. If an assertion failure is found, a counterexample may be given to the user showing how the assertion can be violated. If no warning is given by the SMTChecker for a property, it means that the property is safe.

3. Other checks: Arithmetic underflow and overflow, Division by zero, Trivial conditions and unreachable code, Popping an empty array, Out of bounds index access, Insufficient funds for a transfer.

---

Slide Screenshot

---

Slide Deck

• ABI Experimental
  • SMT Checker
• Not Enabled By Default
• Safety Checks -> SMT Solvers
• Checks:
  • require/assert
  • Overflows/Underflow
  • Divide by zero
  • Unreachable Code
  • etc.
• Affects Security & Optimizations

---

References

• Youtube Reference
• SolidityLang - SMTChecker)