Add a backend function for creating symbolic values representing large integers

[damienmaier]

This feature is needed for the instrumentation of vector instructions in SymQEMU