[acl2/acl2] 269105: [axe/x86] Add theorem to test file.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 26910551e408e158afebee9fa616d812d7bbd495
https://github.com/acl2/acl2/commit/26910551e408e158afebee9fa616d812d7bbd495
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/axe/x86/tests/kestrel/assembly/add.lisp

Log Message:
-----------
[axe/x86] Add theorem to test file.

Based on one proved by the NDSU folks.


Commit: 059d94baaeef13fbf1accca67b58bf2965c21e6b
https://github.com/acl2/acl2/commit/059d94baaeef13fbf1accca67b58bf2965c21e6b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/axe/x86/tests/kestrel/assembly/add.lisp

Log Message:
-----------
[axe/x86] Add theorem to test file.

Based on one proved by the NDSU folks.


Commit: 837f965c96ee505b83339a5f5e887b3ede47b5a6
https://github.com/acl2/acl2/commit/837f965c96ee505b83339a5f5e887b3ede47b5a6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/bv/bvcount.lisp

Log Message:
-----------
[bv] Add rule connecting bvcount to logcount.


Commit: 2273caf64208f18bd1b587fff95bbf547d9fcdb6
https://github.com/acl2/acl2/commit/2273caf64208f18bd1b587fff95bbf547d9fcdb6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/bv/bvchop.lisp

Log Message:
-----------
[bv] Improve a rule.


Commit: bcb3dc6579f4d7a211b1198d61b39a9d9c1db745
https://github.com/acl2/acl2/commit/bcb3dc6579f4d7a211b1198d61b39a9d9c1db745
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/bv/getbit.lisp

Log Message:
-----------
[bv] Add a rule about evenp.


Commit: d68cdca76840027334835954181ec7a765ffba2b
https://github.com/acl2/acl2/commit/d68cdca76840027334835954181ec7a765ffba2b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/bv/bvcount.lisp

Log Message:
-----------
[bv] Remove subsumed rule.


Commit: 81b2d237b87a26903588da68ce3928e0959755fd
https://github.com/acl2/acl2/commit/81b2d237b87a26903588da68ce3928e0959755fd
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/axe/x86/tests/kestrel/assembly/add.lisp

Log Message:
-----------
[axe/x86] Improve test.

Add proofs about the other flags.


Compare: https://github.com/acl2/acl2/compare/e6ed2b305c5d...81b2d237b87a

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/master

Commit: a857b4866be2e38b5c8ea4af9b571b0288985ba1
https://github.com/acl2/acl2/commit/a857b4866be2e38b5c8ea4af9b571b0288985ba1
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/axe/x86/tests/kestrel/assembly/add.lisp

M books/kestrel/bv/bvchop.lisp
M books/kestrel/bv/bvcount.lisp

M books/kestrel/bv/getbit.lisp

Log Message:
-----------

Merge commit '81b2d237b87a26903588da68ce3928e0959755fd' into HEAD


Compare: https://github.com/acl2/acl2/compare/ffb49dc961a3...a857b4866be2

[acl2buildserver]

Branch: refs/heads/testing