[acl2/acl2] d23358: [axe/x86] Tweak.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: d233588e1f8137ff07fcd53ab3d872a98bd3c4b9
https://github.com/acl2/acl2/commit/d233588e1f8137ff07fcd53ab3d872a98bd3c4b9
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-26 (Thu, 26 Feb 2026)

Changed paths:
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
[axe/x86] Tweak.


Commit: 677c9d3b77157fd5c0dd2b9c356f4022f09dd4d3
https://github.com/acl2/acl2/commit/677c9d3b77157fd5c0dd2b9c356f4022f09dd4d3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-26 (Thu, 26 Feb 2026)

Changed paths:
M books/kestrel/air/model-0/air/correctness.lisp
A books/kestrel/air/model-0/air/example.lisp
M books/kestrel/air/model-0/air/field.lisp
M books/kestrel/air/model-0/air/pfcs-constraints.lisp
M books/kestrel/air/model-0/air/pfcs-lifting.lisp
M books/kestrel/air/model-0/air/traces.lisp
M books/kestrel/air/model-0/language/abstract-syntax.lisp
M books/kestrel/air/model-0/language/dynamic-semantics.lisp
A books/kestrel/air/model-0/language/example.lisp
M books/kestrel/air/model-0/language/static-semantics.lisp
M books/kestrel/air/model-0/library-extensions.lisp
M books/kestrel/air/model-0/top.lisp
M books/projects/set-theory/restrict.lisp

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


Commit: 285a51f087a17f204f08e8f9e88f283727a8d280
https://github.com/acl2/acl2/commit/285a51f087a17f204f08e8f9e88f283727a8d280
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-27 (Fri, 27 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/projects/abnf/parsing-tools/defdefparse.lisp
M books/projects/pfcs/.sys/le...@useless-runes.lsp
M books/projects/pfcs/.sys/par...@useless-runes.lsp
M books/projects/pfcs/.sys/syntax-ab...@useless-runes.lsp
M books/projects/pfcs/abstract-syntax-operations.lisp
M books/projects/pfcs/abstract-syntax-trees.lisp
M books/projects/pfcs/abstract-syntax.lisp
M books/projects/pfcs/convenience-constructors.lisp
M books/projects/pfcs/grammar.lisp
M books/projects/pfcs/lexer.lisp
M books/projects/pfcs/parser.lisp
M books/projects/pfcs/syntax-abstraction.lisp
M books/projects/pfcs/tokenizer.lisp
M books/projects/x86isa/machine/catalogue-data.lisp

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


Commit: 434c6588876ceae92036e51cc720ed4bd19848dd
https://github.com/acl2/acl2/commit/434c6588876ceae92036e51cc720ed4bd19848dd
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/dag-to-term.lisp

Log Message:
-----------
[axe] Add a rule.


Commit: d17e0db25e09140af6d2b1488c925eb353113c36
https://github.com/acl2/acl2/commit/d17e0db25e09140af6d2b1488c925eb353113c36
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
[axe/x86] Improve printing and comments.


Commit: 22a8d1609cdc533d66368d24ca5f1e238a30d9e0
https://github.com/acl2/acl2/commit/22a8d1609cdc533d66368d24ca5f1e238a30d9e0
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M README.md
M all-files.txt
M books/doc/more-topics.lisp
M books/doc/publications.acl2
M books/doc/relnotes.lisp
M books/kestrel/air/model-0/top.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/concrete-syntax.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/printing.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/crypto/primes/koala-bear.lisp
M books/kestrel/ethereum/rlp/top.lisp
M books/kestrel/fty/defmake-self.lisp
M books/kestrel/utilities/defstobj-plus-tests.lisp
M books/misc/check-acl2-exports.lisp
M books/projects/aleo/leo/early-version/definition/concrete-syntax.lisp
M books/projects/aleo/leo/early-version/definition/format-strings.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-and.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-all.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-true.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-if.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-nand.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-nor.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-not.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-or.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-xor.lisp
M books/projects/aleo/vm/circuits/pfcs/field-add.lisp
M books/projects/aleo/vm/circuits/pfcs/field-assert-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-assert-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-checked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-flagged.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-unchecked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-double.lisp
M books/projects/aleo/vm/circuits/pfcs/field-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-if.lisp
M books/projects/aleo/vm/circuits/pfcs/field-inv-checked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-inv-flagged.lisp
M books/projects/aleo/vm/circuits/pfcs/field-mul.lisp
M books/projects/aleo/vm/circuits/pfcs/field-neg.lisp
M books/projects/aleo/vm/circuits/pfcs/field-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-square.lisp
M books/projects/aleo/vm/circuits/pfcs/field-sub.lisp
M books/projects/aleo/vm/circuits/top.lisp
M books/projects/aleo/vm/language/grammar.lisp
M books/projects/pfcs/well-formedness.lisp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
A books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
A books/projects/x86isa/machine/instructions/pmadd.lisp
A books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/system/apply/apply-prim.lisp
M books/system/doc/acl2-doc.lisp
M books/system/to-do.txt
M books/workshops/2025/kwan/rv-state.lisp
M defpkgs.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp

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


Commit: 845980b39d829c0895e8ff0fd5d1bd09275af5a7
https://github.com/acl2/acl2/commit/845980b39d829c0895e8ff0fd5d1bd09275af5a7
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/renaming-array.lisp

Log Message:
-----------
[axe] Fix comment typo.


Commit: 8e5538aea61322f534b5e9a5f8320c8c2f343186
https://github.com/acl2/acl2/commit/8e5538aea61322f534b5e9a5f8320c8c2f343186
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/dag-arrays.lisp

Log Message:
-----------
[axe] Improve hint.


Commit: db6b0b4505f738950ec53057fab23704d6034cff
https://github.com/acl2/acl2/commit/db6b0b4505f738950ec53057fab23704d6034cff
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/normalize-xors.lisp

Log Message:
-----------
[axe] Simplify and handle todos.


Commit: 4659e266fae7b4b03fd2f491db89f1a3451b1239
https://github.com/acl2/acl2/commit/4659e266fae7b4b03fd2f491db89f1a3451b1239
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/make-rewriter-simple.lisp

Log Message:
-----------
[axe] Add/organize rules about bounded-darg-listp.


Commit: 8372c8adaac98d48b7e0dceeae1aebf4baa43f1c
https://github.com/acl2/acl2/commit/8372c8adaac98d48b7e0dceeae1aebf4baa43f1c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/dargp.lisp
M books/kestrel/axe/prune-with-contexts.lisp

Log Message:
-----------
[axe] Start making a more abstract interface to dargs.


Commit: 0ad128f64645dabe503fee0dba299b1b58597d7a
https://github.com/acl2/acl2/commit/0ad128f64645dabe503fee0dba299b1b58597d7a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/dag-exprs.lisp

Log Message:
-----------
[axe] Add todo.


Commit: 1f860929d32cb27a4bfbbe5367da0c01120369d7
https://github.com/acl2/acl2/commit/1f860929d32cb27a4bfbbe5367da0c01120369d7
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/dags.lisp

Log Message:
-----------
[axe] Drop duplicate rule.


Commit: d1ddfa351605cc97d92b3f2bdb536ebec5a0d9a1
https://github.com/acl2/acl2/commit/d1ddfa351605cc97d92b3f2bdb536ebec5a0d9a1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-array.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp

Log Message:
-----------
[axe] Simplify hints.


Commit: 00e2994d106138e73e7136aaa93e56b6c508561e
https://github.com/acl2/acl2/commit/00e2994d106138e73e7136aaa93e56b6c508561e
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/bounded-darg-listp.lisp

Log Message:
-----------
[axe] Keep some rules disabled.


Commit: af25312a51804268deb726ecf68cd381be163d39
https://github.com/acl2/acl2/commit/af25312a51804268deb726ecf68cd381be163d39
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/dag-arrays.lisp

Log Message:
-----------
[axe] Improve var names in rules.

Also add bounded-darg-listp-of-take.


Commit: 2dcf1f2c10f415abd2d1e9076109f9f5e8a32e17
https://github.com/acl2/acl2/commit/2dcf1f2c10f415abd2d1e9076109f9f5e8a32e17
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/merge-term-into-dag-array-basic.lisp

Log Message:
-----------
[axe] Speed up proofs a bit.


Commit: 3e850d56e343ef7b8cc001ed524eb67773d782a4
https://github.com/acl2/acl2/commit/3e850d56e343ef7b8cc001ed524eb67773d782a4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/arm/doc.lisp

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


Commit: 4f654f2eea72758ff7db3ead5b60b72f87217b0b
https://github.com/acl2/acl2/commit/4f654f2eea72758ff7db3ead5b60b72f87217b0b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/dag-arrays.lisp

Log Message:
-----------
[axe] Improve implementation.

Disable and comment out some rules.


Commit: a3a3cab1e8403fe8ebaaa4e84353740f35317357
https://github.com/acl2/acl2/commit/a3a3cab1e8403fe8ebaaa4e84353740f35317357
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
[axe/x86] Tweak implementation.


Commit: c9aa4b1f0f0ee57ab232becc3f85e1355471e8a1
https://github.com/acl2/acl2/commit/c9aa4b1f0f0ee57ab232becc3f85e1355471e8a1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-exprs.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp

Log Message:
-----------
[axe] Continue improving implementation rules.


Commit: 07240c07f35e41f1fd339f4cda6ce44bececbc79
https://github.com/acl2/acl2/commit/07240c07f35e41f1fd339f4cda6ce44bececbc79
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/dag-exprs.lisp

Log Message:
-----------
[axe] Continue improving implementation rules.


Commit: 05b9401249e38e6d04a697609905e1723dc1078c
https://github.com/acl2/acl2/commit/05b9401249e38e6d04a697609905e1723dc1078c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/utilities/defstobj-plus-tests.lisp

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


Compare: https://github.com/acl2/acl2/compare/9431757cf3cc...05b9401249e3

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

[acl2buildserver]

Branch: refs/heads/master

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

Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp

M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-exprs.lisp

M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-array.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp

M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/dargp.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-term-into-dag-array-basic.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/renaming-array.lisp

M books/kestrel/axe/x86/unroller.lisp

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

Merge commit '05b9401249e38e6d04a697609905e1723dc1078c' into HEAD


Compare: https://github.com/acl2/acl2/compare/cbb7831b9eb8...d9151ad52212

[acl2buildserver]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-user-01

Commit: 7f63d2bf2d4355494d0755ecf039391c4b83c5e6
https://github.com/acl2/acl2/commit/7f63d2bf2d4355494d0755ecf039391c4b83c5e6
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
A books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp

Log Message:
-----------
[X86ISA] Refactor some code.

Move the SSE and VEX bitwise logical operations to a separate file.


Commit: d443b2591d38d4a51403b38fb204049a6ff6a663
https://github.com/acl2/acl2/commit/d443b2591d38d4a51403b38fb204049a6ff6a663
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/logical.lisp

Log Message:
-----------
[X86ISA] Add PAND/PANDN/POR/PXOR (MMX variants).

Commit: 459cfff321d689df16355b2c3d8b28e862c975e2
https://github.com/acl2/acl2/commit/459cfff321d689df16355b2c3d8b28e862c975e2
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
A books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/top.lisp

Log Message:
-----------
[X86ISA] Refactor some code.

Move packed shifts into new file.


Commit: a76fd6246a389abb535d85b4d3b58993636449b4
https://github.com/acl2/acl2/commit/a76fd6246a389abb535d85b4d3b58993636449b4
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp

Log Message:
-----------
[X86ISA] Move PSLLDQ/PSLRDQ to more appropriate file.


Commit: 8a6d50a0da4d776acf24d48394d34c00ec22484e
https://github.com/acl2/acl2/commit/8a6d50a0da4d776acf24d48394d34c00ec22484e
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/instructions/pshift.lisp

Log Message:
-----------
[X86ISA] Fix comment.


Commit: 1d2c19ba0cc6ad94ce5a0762966cd5ba67d22780
https://github.com/acl2/acl2/commit/1d2c19ba0cc6ad94ce5a0762966cd5ba67d22780
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/instructions/pshift.lisp

Log Message:
-----------
[X86ISA] Refactor some code.

In the packed shift SSE instructions, extract and use a separate macro to
generate the specification functions, so they can be used for other variants of
these instructions (e.g. MMX, upcoming).


Commit: 85ac411190522bbc64f5163eb5559b69e6184a23
https://github.com/acl2/acl2/commit/85ac411190522bbc64f5163eb5559b69e6184a23
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-exprs.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-array.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/dargp.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-term-into-dag-array-basic.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/x86/unroller.lisp

M books/kestrel/utilities/defstobj-plus-tests.lisp
M books/std/obags/core.lisp
M books/std/obags/tests.lisp

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


Compare: https://github.com/acl2/acl2/compare/cbb7831b9eb8...85ac41119052