boehmes [Tue, 30 Nov 2010 18:22:43 +0100] rev 40828
split up Z3 models into constraints on free variables and constant definitions;
reduce Z3 models by replacing unknowns with free variables and constants from the goal;
remove occurrences of the hidden constant fun_app from Z3 models