Example 3: defense against evil
Prerequisite read for this tutorial example is tutorial.
The third evil example is from one of the reviews we get when we first published our paper in Smtlink.
(acl2::must-fail (defthm non-theorem (implies (and (real/rationalp x) (real/rationalp y) (integerp (/ x y))) (not (equal y 0))) :hints (("Goal" :smtlink nil)) :rule-classes nil))
This is an evil theorem because we know below is a theorem in ACL2:
Therefore if Smtlink falsely prove
Smtlink fails to prove the
HARD ACL2 ERROR in SMT-TRANSLATOR=>TRANSLATE-FUNCTION: Not a basic SMT function: INTEGERP
This is because ACL2 treats