The Z3 theorem prover currently has broken OCaml bindings. Attempts by myself at building these bindings using the BAP supplied build procedure (see
$BAP/solvers/getz3.sh in the BAP distribution) have not been successful, so Z3 is currently considered unsupported.
The Binary Analysis Platform only has support for x86 (32 bit) and AMD processors.
For x86, the FPU and MMX instructions have not been modelled in BAP IL (these translate to BAP IL unknowns). Moreover, INT instructions are currently translated to BAP IL special instructions. By accessing the kernel code within a Volatility image, this latter restriction can be overcome.
BAP appears to be primarily designed(?) to operate on code traces/straight line code (e.g. as extracted by PIN). As a result, a number of program analysis techniques have implementations that inadequately handle looping conditions (e.g. WPs and VSA) - these are partially handled using the
unroll(num) BAP commands.