CASE-SPLIT-LIMITATIONS.html -- ACL2 Version 3.1

CASE-SPLIT-LIMITATIONS

a list of two ``numbers'' limiting the number of cases produced at once

Major Section:  MISCELLANEOUS

Examples:
ACL2 !>(case-split-limitations (w state))
(500 100)

With the setting above, clausify will not try subsumption/replacement if more than 500 clauses are involved. Furthermore, the simplifier, as it sweeps over a clause, will inhibit further case splits when it has accumulated 100 subgoals. This inhibition is implemented by continuing to rewrite subsequent literals but not splitting out their cases. This can produce literals containing IFs.

See set-case-split-limitations for a more general discussion.