Add Z3 Interpolation and CHC Support

[baierd]

Z3 supports interpolation again (using model-based interpolants) by utilizing their CHC backend (Spacer). It has to be compiled with a special flag for that. We can add this back in and also enable the usage of Spacer at the same time.