some fixes

- recognize Expr.fls and Expr.emp as pure (for smt calls)
- don't forget pure parts while executing a statement
- [Prover.is_entailment] failed when hypothesis had pure parts; it's
  now temporarily "fixed"
- translate [Expr.emp] and [Expr.fls] into what z3 understands
- assert vars are in one of the recognized categories
- printing of expressions