Implement maps for CVC4, now that it supports constant arrays

reactivate tests for CVC4, if available. Remove non-linear testcase that
worked only on z3 (SumAndMax)
Restore FunDef.orig
Reintroduce liftClosures