• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
      • 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
        • Run-script
        • Std/testing
    • Cgen
    • ACL2s-defaults

    Cgen-single-test-timeout

    Cgen/Testing timeout for single, individual tests (in seconds)

    Maximum allowed time (in seconds) for Cgen to check a single test. The default timeout limit is set to 1/100 sec. This is useful if you have functions that are very slow on some inputs. A simple example is the naive definition of the fibonnaci function. Setting this parameter to 0 amounts to disabling the timeout. Guard : Timeout should be a non-negative rational.
    Usage: 
    (acl2s-defaults :set cgen-single-test-timeout 10) 
    (acl2s-defaults :get cgen-single-test-timeout) 
    :doc cgen-single-test-timeout