Bottom line is: VEX is not supported on a 64bit OS.
However, you may be able to get it to work if
(1) you install the 32-bit compatibility libraries
(2) you change the "as" and "ld" scripts to pass "-m32" to the native C compiler. If you read the book appendix, you'll discover that 'cc' actually invokes the VEX C compiler (*not* gcc, by any means!) and then 'as' on the .s file, which in turn calls 's2cs' (the compiled simulator) and then the native gcc on the cs-annotated C file (the .cs.c file). This last step is where you want to pass the '-m32' flag to gcc
(3) you change the "ld" script to load libraries from /lib32 (or wherever your linux distro installs them). If all goes well, this may already be achieved by step (2)
Cross your fingers and post your results if it works...
-- Paolo