Manipulate characteristics, and property models of bit-vector operations and characteristic models (in the context of an abstract property).