Explanation of failure for instantiate, use in enumerative instantiation (#5951)

Explanation of failure for instantiate, use in enumerative instantiation (#5951)

This makes enumerative instantiation generalize the failures in Instantiate::addInstantiate and increment its enumeration accordingly.

This leads to (+104-6) using enumerative instantiation only on SMT-LIB quantified benchmarks, 60 second timeout.

This is in preparation for further improvements to enumerative instantiation.