pub const BTOR_OPT_NORMALIZE: BtorOption = 23;