Major Section: MISCELLANEOUS
Examples: ACL2 !>(case-split-limitations (w state)) (500 100)With the setting above,
clausifywill 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
See set-case-split-limitations for a more general discussion.