• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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-local-timeout

Cgen/Testing timeout (in seconds)

Maximum allowed time (in seconds) for Cgen to search for counterexamples to a particular form/subgoal. The default timeout limit is set to 10 sec. Setting this parameter to 0 amounts to disabling the timeout mechanism, i.e. its a no-op. Guard : Timeout should be a non-negative rational.

Usage: 
(acl2s-defaults :set cgen-local-timeout 10) 
(acl2s-defaults :get cgen-local-timeout) 
:doc cgen-local-timeout