MRSolver SpecM bugfixes

[m-yac]

This PR makes bugfixes to MRSolver to get as many of the heapster-saw/examples as we can working with the current definition of SpecM. Namely:

• Abstracting uvars at the proper time in mrFreshCallVars
• Giving the proper type to the dummy proof object made in the MaybeElim case of mrRefines
• Adding liftCompStack to monMacro0
• Adding IsLifted argument to FunBind, adding liftStackS case to normComp, and lifting when using normBind in mrRefines'
• Updating SpecPrims.cry, specPrims.saw, and arrays.sawcore to use SpecM instead of CompM
• Adding back MRSolver logic for atM/updateM

This PR also uncomments all the MRSolver tests from the heapster-saw/examples/Makefile, commenting out the only two tests that we aren't able to get working with the current definition of SpecM: zero_array |= zero_array_loop_spec and zero_array |= zero_array_spec from arrays_mr_solver.saw.

[bboston7]

Looks good!