• 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
          • Ccg
          • Defdata
          • ACL2s-user-guide
          • ACL2s-tutorial
          • ACL2s-implementation-notes
          • Match
          • ACL2s-faq
          • ACL2s-intro
          • ACL2s-defaults
            • 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
            • Sampling-method
            • Recursively-fix
            • Num-counterexamples
            • Backtrack-limit
            • Print-cgen-summary
            • Backtrack-bad-generalizations
            • Use-fixers
          • 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-witnesses

Number of Witnesses to be shown

Set the number of witnesses desired to be shown 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-witnesses 3) 
(acl2s-defaults :get num-witnesses) 
:doc num-witnesses