SMT solves with functions for free varibles So this sounds like this might lead to an undecidable theory but I thought I would give it a try and ask about it after I found nothing on the subject. I am somewhat interested in finding functions which are counter examples to predicates (or solutions to the inverse rather). I would like to restrict the functions to some small class however (possibly even smaller than primitive recursive) so I think there is hope of this working if I restrict them enough.

Has any work been done in this area? Have any tools been written for such things?
SMT solvers do support uninterpreted-functions as part of many logics. If there's a counter-example, then they will also print a "counter-example" function, which will be the predicate you're looking for. If you have a concrete example, we can surely see if one can be coded up using Z3.