pub const BTOR_OPT_OUTPUT_NUMBER_FORMAT: BtorOption = 4;