A tutorial to walk you through how to use Smtlink to prove ACL2 theorems.
Following instructions in :doc Smtlink, one should have setup the configuration in file smtlink-config and have certified the Smtlink book afterwards to bake in the configurations.
Then the header of the ACL2 script should look like:
(in-package "ACL2") (include-book "projects/smtlink/top" :dir :system) (tshell-ensure)
Smtlink uses a sequence of computed hints and clause processors to perform different stages. In order to install the computed-hint, one needs to add-default-hints.
(add-default-hints '((SMT::SMT-computed-hint clause)))
The rest of this document contains four pieces of arithmetic examples to
show what one can do with