THEORY ints     ;
LOGIC QF_LIA    ;
SOLVER external ;
SIGNATURE

__init, f1_0_main_Load, f81_0_loop_EQ, !INTEGER;

RULES
f1_0_main_Load(arg1, arg2) -> f81_0_loop_EQ(arg1P, rndarg2P) [(((arg1 > 0) /\ (arg2 > -1)) /\ (arg2 = arg1P))];
f81_0_loop_EQ(arg1, arg2) -> f81_0_loop_EQ(arg1P, rndarg2P) [(((arg1 < 0) /\ (arg1 > -3)) /\ ((arg1 + 2) = arg1P))];
f81_0_loop_EQ(arg1, arg2) -> f81_0_loop_EQ(arg1P, rndarg2P) [(((arg1 > 0) /\ (arg1 < 3)) /\ ((arg1 - 2) = arg1P))];
f81_0_loop_EQ(arg1, arg2) -> f81_0_loop_EQ(arg1P, rndarg2P) [((((arg1 < -2) /\ (arg1 < -1)) /\ (arg1 < 0)) /\ (((-1 * arg1) - 2) = arg1P))];
f81_0_loop_EQ(arg1, arg2) -> f81_0_loop_EQ(arg1P, rndarg2P) [((arg1 > 2) /\ (((-1 * arg1) + 2) = arg1P))];
__init(arg1, arg2) -> f1_0_main_Load(rndarg1P, rndarg2P) [true];
NON-STANDARD IRREGULAR
QUERY loops __init(arg1, arg2)
END OF FILE