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