NOTE-2-7-GUARDS

ACL2 Version 2.7 Notes on Guard-related Changes
Major Section:  NOTE-2-7

It was possible for guard verification to succeed where it should have failed. See the discussion under note-2-7-bug-fixes.

There have been changes in the guards generated from type declarations for the following cases. Thanks to Dave Greve and Matt Wilding for suggesting such changes.

(type (signed-byte n) val)
(type (unsigned-byte n) val)
(type (integer m n) val)
The following examples illustrate the changes.
(type (signed-byte 4) x)
==> [old] (AND (INTEGERP X) (<= -8 X) (<= X 7))
==> [new] (SIGNED-BYTE-P 4 X)

(type (unsigned-byte 4) x) ==> [old] (AND (INTEGERP X) (<= 0 X) (<= X 15)) ==> [new] (UNSIGNED-BYTE-P 4 X)