• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
      • Break-rewrite
      • Proof-builder
      • Accumulated-persistence
      • 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
        • Forward-chaining-reports
        • Proof-tree
        • Print-gv
        • Dmr
        • With-brr-data
        • Splitter
        • Guard-debug
        • Set-debugger-enable
        • Redo-flat
        • Time-tracker
        • Set-check-invariant-risk
        • Removable-runes
        • Efficiency
        • Explain-near-miss
        • Tail-biting
        • Failed-forcing
        • Sneaky
        • Invariant-risk
        • Failure
        • Measure-debug
        • Dead-events
        • Compare-objects
        • Prettygoals
        • Remove-hyps
        • Type-prescription-debugging
        • Pstack
        • Trace
        • Set-register-invariant-risk
        • Walkabout
        • Disassemble$
        • Nil-goal
        • Cw-gstack
        • Set-guard-msg
        • Find-lemmas
        • Watch
        • Quick-and-dirty-subsumption-replacement-step
        • Profile-all
        • Profile-ACL2
        • Set-print-gv-defaults
        • Minimal-runes
        • Spacewalk
        • Try-gl-concls
        • Near-misses
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • 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.