disabled quantifier merging, except when no triggers are provided (as discussed with Rustan)
Fixed abstract interpretation for reals
resolved expressions created during generation of procedures for mover checks
Added /printFixedPoint option
Merge changes for /printFixedPoint option
added more types to constructed expressions
Merge
Fixed malformed Contracts section
Minor fix to abshoudini
added variable hiding
added annotation on an atomic action about the phases in which it exists
Merge
added the framing for the refinement check
fixed some bugs in the previous check ins