pub const BTOR_OPT_FUN_JUST: BtorOption = 29;