• 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

Num-print-witnesses

Number of Witnesses to be printed

Set the number of witnesses desired to be printed. By default this parameter is set to 3. Can be set to any natural number. Setting this number to 0 implies the user is not interested in seeing witnesses, and thus none will be printed in the testing output.

Usage: 
(acl2s-defaults :set num-print-witnesses 3) 
(acl2s-defaults :get num-print-witnesses) 
:doc num-print-witnesses