Class hierarchy:

  prop_convt
   |
  equalityt
   |
  congruence_closuret
   |
  arrayst
   |
  boolbvt
   |
  bv_pointerst
