remember finite mappings in opaque functions

This pull request:
* Remembers finite mappings in opaque functions to help rebuilding counterexamples
* Add examples
* Remove wrong message "Unable to find counterexample"