pub const BTOR_OPT_DECLSORT_BV_WIDTH: BtorOption = 89;