spacer would drop variables of sorts not handled by main loop. - projection with witness needs to disable qel style preprocessing to ensure witnesses are returned. - add euf plugin to handle uninterpreted sorts (and then uninterpreted functions)
