[acl2/acl2] 152881: [axe/x86] Clarify with-supporters issue.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 152881c3b8ad0dbd9c57d818412d5572e267193f
https://github.com/acl2/acl2/commit/152881c3b8ad0dbd9c57d818412d5572e267193f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-23 (Tue, 23 Dec 2025)

Changed paths:
R books/kestrel/axe/x86/tester-code-only.lisp
A books/kestrel/axe/x86/with-supporters-issue.lisp

Log Message:
-----------
[axe/x86] Clarify with-supporters issue.


Commit: 7e6a08f535c5ca56ead0ddd8e52f22acb881ecc6
https://github.com/acl2/acl2/commit/7e6a08f535c5ca56ead0ddd8e52f22acb881ecc6
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-23 (Tue, 23 Dec 2025)

Changed paths:
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/leaves-of-normalized-bitxor-nest.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv-lists/bv-arrays.lisp
M books/kestrel/bv/bif.lisp
M books/kestrel/bv/bitand.lisp
M books/kestrel/bv/bitnot.lisp
M books/kestrel/bv/bitor.lisp
M books/kestrel/bv/bitwise.lisp
M books/kestrel/bv/bitxnor.lisp
M books/kestrel/bv/bitxor.lisp
M books/kestrel/bv/bvand.lisp
M books/kestrel/bv/bvcat-rules.lisp
M books/kestrel/bv/bvcat.lisp
M books/kestrel/bv/bvchop.lisp
M books/kestrel/bv/bvcount.lisp
M books/kestrel/bv/bvif2.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvmult.lisp
M books/kestrel/bv/bvnot.lisp
M books/kestrel/bv/bvor.lisp
M books/kestrel/bv/bvplus.lisp
M books/kestrel/bv/bvsx-rules.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/bvxor.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/bv/if-becomes-bvif-rules.lisp
M books/kestrel/bv/leftrotate-rules.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/logext.lisp
M books/kestrel/bv/putbits.lisp
M books/kestrel/bv/rules2.lisp
M books/kestrel/bv/rules6.lisp
M books/kestrel/bv/sbvlt-rules.lisp
M books/kestrel/bv/sbvlt.lisp
M books/kestrel/bv/sbvrem-rules.lisp
M books/kestrel/bv/single-bit.lisp
M books/kestrel/bv/trim-intro-rules.lisp
M books/kestrel/bv/validation-smt-lib.lisp

Log Message:
-----------
Merge.


Commit: 2a6919589881dcf183142bb565e9b9829a2fe767
https://github.com/acl2/acl2/commit/2a6919589881dcf183142bb565e9b9829a2fe767
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-24 (Wed, 24 Dec 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp

Log Message:
-----------
[axe] Extend list of imported symbols.


Commit: 8658754efa848e49eff09e673a270f9df815f22b
https://github.com/acl2/acl2/commit/8658754efa848e49eff09e673a270f9df815f22b
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-24 (Wed, 24 Dec 2025)

Changed paths:
M books/kestrel/x86/support-bv.lisp

Log Message:
-----------
[x86] Drop unneeded rule.


Commit: 0c0132f1d25dec75f599f7ce33f401760d96e50c
https://github.com/acl2/acl2/commit/0c0132f1d25dec75f599f7ce33f401760d96e50c
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-24 (Wed, 24 Dec 2025)

Changed paths:
A books/kestrel/axe/x86/tester-code-only.lisp

Log Message:
-----------
[axe/x86] Continue working on code-only version of tester.


Commit: 0b0132ad81ea5e4cde77798962abafe3bece2f35
https://github.com/acl2/acl2/commit/0b0132ad81ea5e4cde77798962abafe3bece2f35
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-24 (Wed, 24 Dec 2025)

Changed paths:
M books/kestrel/axe/make-axe-rules.lisp
M books/kestrel/axe/x86/tester.lisp

Log Message:
-----------
Merge.


Compare: https://github.com/acl2/acl2/compare/2efada4e4a0f...0b0132ad81ea

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

[Eric W. Smith]

Branch: refs/heads/master

[Eric W. Smith]

Branch: refs/heads/testing