Added blockpc to souper

This patch addresses issue #81 by implementing blockpc based on Peter's
suggestion. blockpc has the same semantics as pc, except that pc only
applies when the given predecessor of the given block is chosen.
blockpc(s) are collected in a way similar to what we currently do for pc(s),
and are encoded with a similar technique for encoding UB constraints.

The parser is also updated to parse blockpc(s).
Merge pull request #136 from rsas/bump-klee

Remove ExprSMTLIBLetPrinter
Merge pull request #98 from chenyang78/blockpc

Blockpc
remove support for n-ary associative operators, in order to retain a closer
mapping between LLVM and Souper IRs
Merge pull request #137 from regehr/no-nary-operators

remove the n-ary associative operators
Remove unused code line
Merge pull request #138 from rsas/unused-expr

Remove unused code line
Make field order consistent with ctor initialisation order
Merge pull request #143 from jeroenk/order

Make field order consistent with ctor initialisation order
Handle instruction UB on the RHS correctly
Add a note how to speed up SMT query solving
Merge pull request #145 from rsas/bv-note

Add a note how to speed up SMT query solving
Merge pull request #133 from rsas/rhs-ub

Handle instruction UB on the RHS correctly
Merge branch 'master' into iN-no-quantifiers

Conflicts:
	include/souper/Extractor/KLEEBuilder.h
	lib/Extractor/Solver.cpp