[acl2/acl2] f0560e: Add AND instruction properties with global cert.acl2

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: f0560e56579615e7de70cf8300711750938858ee
https://github.com/acl2/acl2/commit/f0560e56579615e7de70cf8300711750938858ee
Author: Yusuf Moshood <yusuf....@ndus.edu>
Date: 2026-06-30 (Tue, 30 Jun 2026)

Changed paths:
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/acl2-customization.lsp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_bl_8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_bl_8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_bl_8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_mem8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_mem8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_mem8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_bx_16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_bx_16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_bx_16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_mem16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_mem16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_mem16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bl_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bl_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bl_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_ebx_32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_ebx_32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_ebx_32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_mem32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_mem32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_mem32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_ax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_ax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_ax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_eax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_eax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_eax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_rax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_rax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_rax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_al.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_al.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_al.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_mem64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_mem64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_mem64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_rbx_64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_rbx_64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_rbx_64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/cert.acl2

Log Message:
-----------
Add AND instruction properties with global cert.acl2


Commit: db70b980e2153ce83259807925d2f26460a4643d
https://github.com/acl2/acl2/commit/db70b980e2153ce83259807925d2f26460a4643d
Author: Yusuf Moshood <yusuf....@ndus.edu>
Date: 2026-06-30 (Tue, 30 Jun 2026)

Changed paths:
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_al_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_al_mem8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_mem16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_bl_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_bx_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_eax_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_eax_mem32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ebx_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_ax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_eax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_rax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem8_al.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem8_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rax_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rax_mem64.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rbx_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/al_bl_8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/ax_bx_16.acl2
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/cert.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/eax_ebx_32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/rax_rbx_64.acl2
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/cert.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_bl_8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_mem8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_bx_16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_mem16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bl_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_ebx_32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_mem32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ebx_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ebx_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_ax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_eax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_rax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem8_al.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem8_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_mem64.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_rbx_64.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rbx_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rbx_imm8.acl2

Log Message:
-----------
Replace individual .acl2 files with global cert.acl2 in add and sub directories

Co-Authored-By: Claude Sonnet 5 <nor...@anthropic.com>


Commit: ab3656aa762367c9618dc854a744cc8d32e579cd
https://github.com/acl2/acl2/commit/ab3656aa762367c9618dc854a744cc8d32e579cd
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>
Date: 2026-06-30 (Tue, 30 Jun 2026)

Changed paths:
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_al_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_al_mem8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_mem16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_bl_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_bx_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_eax_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_eax_mem32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ebx_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_ax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_eax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_rax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem8_al.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem8_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rax_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rax_mem64.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rbx_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/al_bl_8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/ax_bx_16.acl2
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/cert.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/eax_ebx_32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/rax_rbx_64.acl2
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/acl2-customization.lsp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_bl_8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_bl_8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_bl_8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_mem8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_mem8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_mem8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_bx_16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_bx_16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_bx_16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_mem16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_mem16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_mem16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bl_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bl_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bl_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_ebx_32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_ebx_32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_ebx_32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_mem32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_mem32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_mem32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_ax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_ax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_ax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_eax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_eax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_eax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_rax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_rax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_rax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_al.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_al.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_al.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_mem64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_mem64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_mem64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_rbx_64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_rbx_64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_rbx_64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/cert.acl2
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/cert.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_bl_8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_mem8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_bx_16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_mem16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bl_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_ebx_32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_mem32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ebx_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ebx_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_ax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_imm16.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_eax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_rax.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem8_al.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem8_imm8.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_mem64.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_rbx_64.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rbx_imm32.acl2
R books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rbx_imm8.acl2

Log Message:
-----------
Merge pull request #1966 from mayuf413/testing-kestrel

AND instruction properties with global cert.acl2


Compare: https://github.com/acl2/acl2/compare/98dbacf7ab8a...ab3656aa7623

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