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

Max number of tries to find counterexamples

Maximum number of tries (attempts) to construct counterexamples and witnesses. By default this parameter is set to 4000. Can be set to any natural number n. If set to 0, it is similar to setting testing-enabled parameter to nil.

Usage: 
(acl2s-defaults :set num-trials 4000) 
(acl2s-defaults :get num-trials) 
:doc num-trials