Added tests for LIA and UF. UF model parsing in mathsat does not work.