Modified how S2 expressions are exported via JSON to include more sort information for a constraint solver.
Changed s2exp normilization to ignore s2var when exporting constraints. The reasoning behind this is that when we replace s2var's with expressions they represent, the SMT solver is unable to understand equality between two static variables.