Need to Specify -m32 when Compiling Example on 64-Bit Linux

[domainexpert]

In the README.md there is an instruction to compile sign32.c as follows.

gcc -Ivalgrind-x.x.x/taintgrind/ -Ivalgrind-x.xx.x/include/ -g sign32.c -o sign32

However, compiling in the above manner resulted in Z3 errors (on x86_64 Ubuntu 14.04 Linux 3.19.0).

(error "line 25 column 29: Sorts (_ BitVec 32) and (_ BitVec 64) are incompatible")
(error "line 40 column 28: Sorts (_ BitVec 32) and (_ BitVec 64) are incompatible")
(error "line 67 column 30: Sorts (_ BitVec 32) and (_ BitVec 64) are incompatible")
...
(error "line 104 column 30: Sorts (_ BitVec 32) and (_ BitVec 64) are incompatible")
unsat
(error "line 127 column 10: model is not available")

with only one solution produced by Z3. The error disappeared when I included -m32 option when compiling sign32.c in the following way:

gcc -Ivalgrind-x.x.x/taintgrind/ -Ivalgrind-x.xx.x/include/ -m32 -g sign32.c -o sign32

The same problem and resolution apply to sign64.c as well. Perhaps README.md should indicate that -m32 may be needed.