THEORY ints     ;
LOGIC QF_LIA    ;
SOLVER external ;
SIGNATURE

__init, f1_0_main_Load, f98_0_loop_EQ, !INTEGER;

RULES
f1_0_main_Load(arg1, arg2) -> f98_0_loop_EQ(arg1P, rndarg2P) [(((arg1 > 0) /\ (arg2 > -1)) /\ (arg2 = arg1P))];
f98_0_loop_EQ(arg1, arg2) -> f98_0_loop_EQ(arg1P, rndarg2P) [((((arg1 > -3) /\ (arg1 < 1)) /\ (arg1 < 0)) /\ ((arg1 + 2) = arg1P))];
f98_0_loop_EQ(arg1, arg2) -> f98_0_loop_EQ(arg1P, rndarg2P) [(((arg1 > 0) /\ (arg1 < 3)) /\ ((arg1 - 2) = arg1P))];
f98_0_loop_EQ(arg1, arg2) -> f98_0_loop_EQ(arg1P, rndarg2P) [(((arg1 > 2) /\ ((-1 * arg1) < -1)) /\ (((-1 * arg1) + 2) = arg1P))];
f98_0_loop_EQ(arg1, arg2) -> f98_0_loop_EQ(arg1P, rndarg2P) [((((((arg1 < -1) /\ (arg1 < 0)) /\ (arg1 < -2)) /\ (3 <= (-1 * arg1))) /\ (arg1 < 1)) /\ (((-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