Using SPARK as a Solver for Modelica