• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
          • Note-2-8
          • Note-2-7
          • Note-8-6
          • Note-8-2
          • Note-7-0
          • Note-8-5
          • Note-8-3
          • Note-8-1
          • Note-8-0
          • Note-7-1
          • Note-6-4
          • Note-2-9-3
          • Note-2-9-1
          • Note-8-4
          • Note-7-2
          • Note-6-5
          • Note-4-0
          • Note-2-9-2
          • Note-3-6
          • Note-3-3
          • Note-3-2-1
          • Note-3-0-1
          • Note-2-9-5
          • Note-2-5
          • Note-1-5
          • Note-6-1
          • Note-4-3
          • Note-4-2
          • Note-4-1
          • Note-3-5
          • Note-3-4
          • Note-3-2
          • Note-3-0-2
          • Note-2-9-4
          • Note-2-9
          • Note-1-8
          • Note-1-7
          • Note-1-6
          • Note-1-4
          • Note-1-3
          • Note-7-4
          • Note-7-3
          • Note-6-3
          • Note-6-2
          • Note-6-0
          • Note-5-0
          • Note-8-7
          • Note-1-9
          • Note-2-2
          • Note-1-8-update
          • Note-3-5(r)
          • Note-2-3
          • Release-notes-books
          • Note-3-6-1
          • Note-1-2
          • Note-2-4
          • Note-2-6
          • Note-2-0
          • Note-3-0
          • Note-3-2(r)
          • Note-2-7(r)
          • Note-1-1
          • Note-3-4(r)
          • Note-3-1
          • Note-2-8(r)
          • Note-2-1
          • Note-2-9(r)
          • Note-2-6(r)
          • Note-3-1(r)
          • Note-3-0(r)
          • Note-3-0-1(r)
          • Note-2-5(r)
          • Note-4-3(r)
          • Note-4-2(r)
          • Note-4-1(r)
          • Note-4-0(r)
          • Note-3-6(r)
          • Note-3-3(r)
          • Note-3-2-1(r)
        • Version
        • Acknowledgments
        • Pre-built-binary-distributions
        • Common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
        • ACL2-help
        • Bibliography
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Release-notes

Note-3-6-1

ACL2 Version 3.6.1 (September, 2009) Notes

NOTE! New users can ignore these release notes, because the documentation has been updated to reflect all changes that are recorded here.

The essential changes to ACL2 since Version 3.6 are the two bug fixes described below. There was also some functionality-neutral code refactoring, as requested by Daron Vroon in support of the ACL2 Sedan (see ACL2-sedan). Also see ReleaseVersionNumbers for a list of books in Version 3.6.1 of ACL2 but not Version 3.6. For changes to existing books rather than additions, see the log entries starting with revision r329 up through revision 350.

Fixed a soundness bug in the handling of ruler-extenders, specifically in the handling of let-expressions. Thanks to Pete Manolios, who sent us a proof of nil, essentially as follows. In the termination proof for foo below, the binding of x to (cons t x) was not substituted into the recursive call of foo for purposes of the termination proof.

(defun foo (x)
  (declare (xargs :ruler-extenders :all))
  (let ((x (cons t x)))
    (if (endp (cdr x))
        x
      (cons t (foo (cdr x))))))

(defthm foo-bad
  nil
  :hints (("Goal"
           :use ((:instance foo (x '(3))))
           :in-theory (disable foo (foo))))
  :rule-classes nil)

Fixed a typo in code supporting ruler-extenders (specifically, swapped arguments in a recursive call of ACL2 source function get-ruler-extenders2, which could cause problems for functions defined using mutual-recursion). Thanks to Daron Vroon for bringing this bug to our attention, pointing out the swapped arguments.