		Search-engine friendly clone of the ACL2 documentation.

Tutorial

Example-3

Example 3: defense against evil

Example 3

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:

(thm (equal (/ x 0) 0))

Therefore if Smtlink falsely prove non-theorem, it will introduce contradiction into ACL2.

Smtlink fails to prove the non-theorem with error message:

HARD ACL2 ERROR in SMT-TRANSLATOR=>TRANSLATE-FUNCTION:  Not a basic
SMT function: INTEGERP

This is because ACL2 treats integerp's as type declarations in Z3. But here in this theorem, (integerp (/ x y)) is a constraint/hypotheses rather than a type declaration. When ACL2 tried to translate it as a constraint, it finds out integerp is not a supported function.