New year improvements

• Simplify context: revert ref during pop
• More floating point propagation
• Less quantifiers time by not matching and foing congruence closure on boolean operators.