fixing bug in tuple axioms, better smt model parsing