• 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
        • Introduction-to-the-theorem-prover
        • Pages Written Especially for the Tours
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
          • Defunc
          • Cgen
            • Defdata
            • Test?
            • ACL2s-defaults
            • Prove/cgen
            • Register-type
            • With-timeout
            • Defdata-attach
            • Testing-enabled
            • Defdata-aliasing-enabled
            • Cgen-single-test-timeout
            • Verbosity-level
            • Search-strategy
            • Num-print-counterexamples
            • Cgen-timeout
            • Cgen-local-timeout
            • Num-witnesses
            • Num-trials
            • Num-print-witnesses
            • Test-then-skip-proofs
            • Sampling-method
            • Recursively-fix
            • Num-counterexamples
            • Backtrack-limit
            • Print-cgen-summary
            • Cgen::flush
            • Backtrack-bad-generalizations
            • Use-fixers
            • Thm-no-test
            • Defthmd-no-test
            • Defthm-no-test
          • Ccg
          • Defdata
          • ACL2s-user-guide
          • ACL2s-tutorial
          • ACL2s-implementation-notes
          • Match
          • ACL2s-faq
          • ACL2s-intro
          • ACL2s-defaults
          • Definec
          • ACL2s-utilities
          • ACL2s-interface
          • ACL2s-installation
        • Talks
        • Nqthm-to-ACL2
        • Emacs
      • About-ACL2
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Cgen
• ACL2s-defaults

Recursively-fix

Specify whether unsatisfied but fixable constraints are to be recursively fixed.

Specify whether unsatisfied but fixable constraints are to be recursively fixed. The resulting solution substitutions are stacked in the reverse order. By default this parameter is set to t.