New year improvements

François Bobotrequested to merge
bobot/abs into master
  • Simplify context: revert ref during pop
  • More floating point propagation
  • Less quantifiers time by not matching and foing congruence closure on boolean operators.

Merge request reports