Add Event::encode(const Z3Encoder&, Z3&) virtual function

Use this new function to process a recorded list of write events whose
return types are incompatible, e.g. see Recorder::instr().