var u_EBX_4008e5_blk_ex, >=0, <= 4294967295;
var u_EAX_4008e0_blk_ex_T, >=0, <= 4294967295;
var u_EBX_4008e7_blk_ex, >=0, <= 4294967295;
var l_EAX_4008e0, >=0, <= 4294967295;
var l_EAX_4008e3, >=0, <= 4294967295;
var l_EAX_4008e5, >=0, <= 4294967295;
var l_EAX_4008e7, >=0, <= 4294967295;
var l_EAX_4008e6, >=0, <= 4294967295;
var u_EAX_4008e0_blk_ex_F, >=0, <= 4294967295;
var rch_blk_4008e0_ent, binary;
var u_EAX_4008e5_blk_ex, >=0, <= 4294967295;
var u_EBX_4008e0_blk_ex_F, >=0, <= 4294967295;
var l_EAX_4008e0_blk_ex_T, >=0, <= 4294967295;
var l_EAX_4008e7_blk_ex, >=0, <= 4294967295;
var dcsn_lte_3, binary;
var dcsn_lte_2, binary;
var dcsn_lte_1, binary;
var dcsn_lte_0, binary;
var l_EAX_4008e0_blk_ex_F, >=0, <= 4294967295;
var u_EBX_4008e0_blk_ex_T, >=0, <= 4294967295;
var l_EBX_4008e5_blk_ex, >=0, <= 4294967295;
var rch_blk_4008e0_ex_F, binary;
var u_EBX_4008e0, >=0, <= 4294967295;
var u_EBX_4008e3, >=0, <= 4294967295;
var u_EBX_4008e5, >=0, <= 4294967295;
var u_EBX_4008e7, >=0, <= 4294967295;
var u_EBX_4008e6, >=0, <= 4294967295;
var rch_blk_4008e0_ex_T, binary;
var u_EAX_4008e5, >=0, <= 4294967295;
var rch_blk_4008e0_pred_T, binary;
var l_EBX_4008e7_blk_ex, >=0, <= 4294967295;
var rch_blk_4008e5_ex, binary;
var rch_blk_4008e5_ent, binary;
var u_EAX_4008e3, >=0, <= 4294967295;
var u_EAX_4008e0, >=0, <= 4294967295;
var u_EAX_4008e6, >=0, <= 4294967295;
var u_EAX_4008e7, >=0, <= 4294967295;
var rch_blk_4008e0_pred_F, binary;
var l_EAX_4008e5_blk_ex, >=0, <= 4294967295;
var rch_blk_4008e7_ex, binary;
var l_EBX_4008e0_blk_ex_F, >=0, <= 4294967295;
var l_EBX_4008e3, >=0, <= 4294967295;
var l_EBX_4008e0, >=0, <= 4294967295;
var l_EBX_4008e6, >=0, <= 4294967295;
var l_EBX_4008e7, >=0, <= 4294967295;
var rch_blk_4008e7_ent, binary;
var l_EBX_4008e5, >=0, <= 4294967295;
var u_EAX_4008e7_blk_ex, >=0, <= 4294967295;
var dcsn_and_5, binary;
var dcsn_and_4, binary;
var l_EBX_4008e0_blk_ex_T, >=0, <= 4294967295;
minimize obj_fn: + 1 * u_EAX_4008e0 -1 * l_EAX_4008e0 + 1 * u_EBX_4008e0 -1 * l_EBX_4008e0 + 1 * u_EAX_4008e3 -1 * l_EAX_4008e3 + 1 * u_EBX_4008e3 -1 * l_EBX_4008e3 + 1 * u_EAX_4008e0_blk_ex_T -1 * l_EAX_4008e0_blk_ex_T + 1 * u_EBX_4008e0_blk_ex_T -1 * l_EBX_4008e0_blk_ex_T + 1 * u_EAX_4008e0_blk_ex_F -1 * l_EAX_4008e0_blk_ex_F + 1 * u_EBX_4008e0_blk_ex_F -1 * l_EBX_4008e0_blk_ex_F + 1 * u_EAX_4008e7 -1 * l_EAX_4008e7 + 1 * u_EBX_4008e7 -1 * l_EBX_4008e7 + 1 * u_EAX_4008e7_blk_ex -1 * l_EAX_4008e7_blk_ex + 1 * u_EBX_4008e7_blk_ex -1 * l_EBX_4008e7_blk_ex + 1 * u_EAX_4008e5 -1 * l_EAX_4008e5 + 1 * u_EBX_4008e5 -1 * l_EBX_4008e5 + 1 * u_EAX_4008e6 -1 * l_EAX_4008e6 + 1 * u_EBX_4008e6 -1 * l_EBX_4008e6 + 1 * u_EAX_4008e5_blk_ex -1 * l_EAX_4008e5_blk_ex + 1 * u_EBX_4008e5_blk_ex -1 * l_EBX_4008e5_blk_ex ;

s.t. c0: + 1 * l_EAX_4008e0 -1 * u_EAX_4008e0 <= 0;
s.t. c1: + 1 * l_EBX_4008e0 -1 * u_EBX_4008e0 <= 0;
s.t. c2: + 1 * l_EAX_4008e3 -1 * u_EAX_4008e3 <= 0;
s.t. c3: + 1 * l_EBX_4008e3 -1 * u_EBX_4008e3 <= 0;
s.t. c4: + 1 * l_EAX_4008e3 -1 * l_EAX_4008e0 = 0;
s.t. c5: + 1 * u_EAX_4008e3 -1 * u_EAX_4008e0 = 0;
s.t. c6: + 1 * l_EBX_4008e3 -1 * l_EBX_4008e0 = 0;
s.t. c7: + 1 * u_EBX_4008e3 -1 * u_EBX_4008e0 = 0;
s.t. c8: + 1 * l_EAX_4008e0_blk_ex_T -1 * u_EAX_4008e0_blk_ex_T <= 0;
s.t. c9: + 1 * l_EBX_4008e0_blk_ex_T -1 * u_EBX_4008e0_blk_ex_T <= 0;
s.t. c10: + 1 * l_EAX_4008e0_blk_ex_F -1 * u_EAX_4008e0_blk_ex_F <= 0;
s.t. c11: + 1 * l_EBX_4008e0_blk_ex_F -1 * u_EBX_4008e0_blk_ex_F <= 0;
s.t. c12: + 4294967296 * dcsn_lte_0 -1 * u_EAX_4008e0 <= 4294967291;
s.t. c13: -4294967296 * dcsn_lte_0 + 1 * u_EAX_4008e0 <= 4;
s.t. c14: + 1 * rch_blk_4008e0_pred_T -1 * dcsn_lte_0 = 0;
s.t. c15: -1 * u_EAX_4008e0 + 1 * u_EAX_4008e0_blk_ex_T = 0;
s.t. c16: -1 * l_EAX_4008e0 + 4294967296 * dcsn_lte_1 <= 4294967291;
s.t. c17: + 1 * l_EAX_4008e0 -4294967296 * dcsn_lte_1 <= 4;
s.t. c18: + 1 * l_EAX_4008e0_blk_ex_T -1 * l_EAX_4008e0 + 4294967296 * dcsn_lte_1 <= 4294967296;
s.t. c19: + 1 * l_EAX_4008e0_blk_ex_T -4294967296 * dcsn_lte_1 <= 5;
s.t. c20: + 4294967296 * dcsn_lte_2 + 1 * l_EAX_4008e0 <= 4294967300;
s.t. c21: -4294967296 * dcsn_lte_2 -1 * l_EAX_4008e0 <= -5;
s.t. c22: + 1 * rch_blk_4008e0_pred_F -1 * dcsn_lte_2 = 0;
s.t. c23: -1 * l_EAX_4008e0 + 1 * l_EAX_4008e0_blk_ex_F = 0;
s.t. c24: + 4294967296 * dcsn_lte_3 + 1 * u_EAX_4008e0 <= 4294967300;
s.t. c25: -4294967296 * dcsn_lte_3 -1 * u_EAX_4008e0 <= -5;
s.t. c26: + 4294967296 * dcsn_lte_3 -1 * u_EAX_4008e0_blk_ex_F + 1 * u_EAX_4008e0 <= 4294967296;
s.t. c27: -4294967296 * dcsn_lte_3 -1 * u_EAX_4008e0_blk_ex_F <= -4;
s.t. c28: + 1 * l_EBX_4008e0_blk_ex_T -1 * l_EBX_4008e3 = 0;
s.t. c29: + 1 * u_EBX_4008e0_blk_ex_T -1 * u_EBX_4008e3 = 0;
s.t. c30: + 1 * l_EBX_4008e0_blk_ex_F -1 * l_EBX_4008e3 = 0;
s.t. c31: + 1 * u_EBX_4008e0_blk_ex_F -1 * u_EBX_4008e3 = 0;
s.t. c32: -2 * dcsn_and_4 + 1 * rch_blk_4008e0_ent + 1 * rch_blk_4008e0_pred_T <= 1;
s.t. c33: + 2 * dcsn_and_4 -1 * rch_blk_4008e0_ent -1 * rch_blk_4008e0_pred_T <= 0;
s.t. c34: + 1 * rch_blk_4008e0_ex_T -1 * dcsn_and_4 = 0;
s.t. c35: + 1 * rch_blk_4008e0_pred_F + 1 * rch_blk_4008e0_ent -2 * dcsn_and_5 <= 1;
s.t. c36: -1 * rch_blk_4008e0_pred_F -1 * rch_blk_4008e0_ent + 2 * dcsn_and_5 <= 0;
s.t. c37: + 1 * rch_blk_4008e0_ex_F -1 * dcsn_and_5 = 0;
s.t. c38: + 1 * l_EAX_4008e7 -1 * u_EAX_4008e7 <= 0;
s.t. c39: + 1 * l_EBX_4008e7 -1 * u_EBX_4008e7 <= 0;
s.t. c40: + 1 * l_EAX_4008e7_blk_ex -1 * u_EAX_4008e7_blk_ex <= 0;
s.t. c41: + 1 * l_EBX_4008e7_blk_ex -1 * u_EBX_4008e7_blk_ex <= 0;
s.t. c42: + 1 * l_EAX_4008e7_blk_ex -1 * l_EAX_4008e7 = 0;
s.t. c43: + 1 * u_EAX_4008e7_blk_ex -1 * u_EAX_4008e7 = 0;
s.t. c44: + 1 * l_EBX_4008e7_blk_ex -1 * l_EBX_4008e7 = 0;
s.t. c45: + 1 * u_EBX_4008e7_blk_ex -1 * u_EBX_4008e7 = 0;
s.t. c46: + 1 * rch_blk_4008e7_ex -1 * rch_blk_4008e7_ent = 0;
s.t. c47: + 1 * l_EAX_4008e5 -1 * u_EAX_4008e5 <= 0;
s.t. c48: + 1 * l_EBX_4008e5 -1 * u_EBX_4008e5 <= 0;
s.t. c49: + 1 * l_EAX_4008e6 -1 * u_EAX_4008e6 <= 0;
s.t. c50: + 1 * l_EBX_4008e6 -1 * u_EBX_4008e6 <= 0;
s.t. c51: + 1 * l_EAX_4008e6 -1 * l_EAX_4008e5 = 0;
s.t. c52: + 1 * u_EAX_4008e6 -1 * u_EAX_4008e5 = 0;
s.t. c53: + 1 * l_EBX_4008e6 -1 * l_EBX_4008e5 = 0;
s.t. c54: + 1 * u_EBX_4008e6 -1 * u_EBX_4008e5 = 0;
s.t. c55: + 1 * l_EAX_4008e5_blk_ex -1 * u_EAX_4008e5_blk_ex <= 0;
s.t. c56: + 1 * l_EBX_4008e5_blk_ex -1 * u_EBX_4008e5_blk_ex <= 0;
s.t. c57: + 1 * l_EAX_4008e5_blk_ex -1 * l_EAX_4008e6 = 0;
s.t. c58: + 1 * u_EAX_4008e5_blk_ex -1 * u_EAX_4008e6 = 0;
s.t. c59: + 1 * l_EBX_4008e5_blk_ex -1 * l_EBX_4008e6 = 0;
s.t. c60: + 1 * u_EBX_4008e5_blk_ex -1 * u_EBX_4008e6 = 0;
s.t. c61: + 1 * rch_blk_4008e5_ex -1 * rch_blk_4008e5_ent = 0;
s.t. c62: + 1 * l_EAX_4008e0 = 8;
s.t. c63: + 1 * u_EAX_4008e0 = 9;
s.t. c64: + 1 * l_EBX_4008e0 = 0;
s.t. c65: + 1 * u_EBX_4008e0 = 4294967295;
s.t. c66: + 1 * rch_blk_4008e0_ent = 1;
s.t. c67: + 1 * rch_blk_4008e7_ent -1 * rch_blk_4008e0_ex_T = 0;
s.t. c68: -1 * l_EAX_4008e0_blk_ex_T + 1 * l_EAX_4008e7 + 4294967296 * rch_blk_4008e7_ent <= 4294967296;
s.t. c69: + 4294967296 * rch_blk_4008e7_ent + 1 * u_EAX_4008e0_blk_ex_T -1 * u_EAX_4008e7 <= 4294967296;
s.t. c70: + 4294967296 * rch_blk_4008e7_ent -1 * l_EBX_4008e0_blk_ex_T + 1 * l_EBX_4008e7 <= 4294967296;
s.t. c71: + 1 * u_EBX_4008e0_blk_ex_T + 4294967296 * rch_blk_4008e7_ent -1 * u_EBX_4008e7 <= 4294967296;
s.t. c72: + 1 * rch_blk_4008e5_ent -1 * rch_blk_4008e0_ex_F = 0;
s.t. c73: + 1 * l_EAX_4008e5 + 4294967296 * rch_blk_4008e5_ent -1 * l_EAX_4008e0_blk_ex_F <= 4294967296;
s.t. c74: -1 * u_EAX_4008e5 + 4294967296 * rch_blk_4008e5_ent + 1 * u_EAX_4008e0_blk_ex_F <= 4294967296;
s.t. c75: + 1 * l_EBX_4008e5 + 4294967296 * rch_blk_4008e5_ent -1 * l_EBX_4008e0_blk_ex_F <= 4294967296;
s.t. c76: -1 * u_EBX_4008e5 + 4294967296 * rch_blk_4008e5_ent + 1 * u_EBX_4008e0_blk_ex_F <= 4294967296;