1. Added isUnsat to Extensions.scala
2. Added a few more conditions to BinarySearchTree.scala
3. Made calls to underlying solvers (involving double negation, etc) from the unifier
4. Fixed a minor bug in Expression Parsing in Main.scala