Handle fmf.card as input from user, add support in SMT2 parser, as requested by Martin Brain.  Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental.
Revert E-matching datatypes fix.