• 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

Num-counterexamples

Number of Counterexamples to be searched

Set the number of counterexamples desired to be searched. 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 searching for counterexamples.

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