Clarify rules restricted when generated from CVC4
Haniel indicated that some rules are generated in a stricter variant by CVC4. It is unclear how we will enable reconstructions to benefit from this without writing solver specific routines.
The two big options are: a) have a dedicated rule for the more specialized version b) have optional arguments.
It is probably best to first collect those cases.