• 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-counterexamples

Number of Counterexamples to be printed

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

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