now generating VCs for preconditions and pattern-matching exhaustiveness...

src/purescala/DefaultTactic.scala

src/purescala/PartialEvaluator.scala

src/purescala/Trees.scala

src/purescala/VerificationCondition.scala

src/purescala/Z3Solver.scala

src/purescala/z3plugins/instantiator/Instantiator.scala

testcases/BSTSimpler.scala

testcases/ExprComp.scala

testcases/RedBlackTree.scala