NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: 0, SER4343^0 -> 1, ap_server_conf___03737^0 -> undef34, i^0 -> (0 + undef51), lr^0 -> (0 + ap_listeners^0), my_child_num___04040^0 -> (0 + my_child_num^0), num_listensocks^0 -> undef51, num_listensocks___04646^0 -> (0 + num_listensocks^0), pchild___03636^0 -> undef59, pchild___03939^0 -> undef60, pchild___04747^0 -> undef61, sbh___04242^0 -> undef78, z4141^0 -> 0, z4848^0 -> 0}> 1, tmp3535^0 -> undef185}> ~(1), pollset___06161^0 -> undef769, ret_apr_pollset_poll6666^0 -> undef775, status^0 -> (0 + undef775), tmp6565^0 -> undef790}> 1}> undef1907}> undef2137, current_conn___07575^0 -> (0 + current_conn^0), current_conn___07777^0 -> (0 + current_conn^0), handled_conn^0 -> 1}> undef2609, current_conn^0 -> (0 + undef2609)}> 1, tmp7474^0 -> undef2994}> 1}> 0}> 1, tmp6868^0 -> undef3991}> undef4108}> (0 + undef4597), ret_accept_mutex_off7070^0 -> undef4573, status^0 -> undef4582, tmp6969^0 -> undef4592, tmp7272^0 -> undef4593, tmp___18^0 -> undef4597}> (0 + ap_listeners^0)}> 0, SER5555^0 -> 1, a5959^0 -> (0 + undef4996), do_ACCEPT^0 -> 0, ret_accept_mutex_on5858^0 -> undef4974, sbh___05454^0 -> undef4979, tmp5757^0 -> undef4988, tmp6060^0 -> undef4989, tmp___04^0 -> undef4996}> 0, tmp5353^0 -> undef5188}> (1 + requests_this_child^0), tmp3^0 -> (0 + requests_this_child^0)}> undef5472}> 0, tmp7979^0 -> undef5596}> (~(1) + i^0), pfd___01^0 -> 0, pfd_client_data^0 -> (0 + lr^0), pfd_desc_s^0 -> 1, pfd_desc_type^0 -> 6, pfd_reqevents^0 -> 5, pollset___04949^0 -> undef5669}> 8}> 0, NL2727^0 -> 0, allocator___01414^0 -> undef5819, allocator___01919^0 -> undef5820, allocator___02020^0 -> undef5821, ap_daemons_limit^0 -> 0, ap_daemons_max_free^0 -> 0, ap_daemons_min_free^0 -> 0, ap_daemons_to_start^0 -> 0, ap_listeners^0 -> undef5826, ap_lock_fname___03030^0 -> (0 + ap_lock_fname^0), ap_max_mem_free___01515^0 -> (0 + ap_max_mem_free^0), ap_my_pid^0 -> (0 + undef5878), ap_server_conf___01212^0 -> undef5834, ap_threads_per_child^0 -> 0, child_num_arg^0 -> undef5837, die_now^0 -> 0, do_ACCEPT^0 -> 0, first_server_limit^0 -> 0, handled_conn^0 -> 0, last_poll_idx^0 -> 0, mpm_state^0 -> 9, my_child_num^0 -> (0 + undef5837), pchild___02121^0 -> undef5856, pchild___02323^0 -> undef5857, pchild___02626^0 -> undef5858, pchild___03131^0 -> undef5859, pconf___01717^0 -> undef5863, ptrans___02424^0 -> undef5871, requests_this_child^0 -> 0, ret_apr_proc_mutex_child_init3333^0 -> undef5877, ret_getpid1111^0 -> undef5878, server_limit^0 -> 256, status^0 -> (0 + undef5877), tmp1010^0 -> undef5884, tmp3232^0 -> undef5885, z2828^0 -> 0}> Fresh variables: undef34, undef51, undef59, undef60, undef61, undef78, undef185, undef769, undef775, undef790, undef1907, undef2137, undef2609, undef2994, undef3991, undef4108, undef4573, undef4582, undef4592, undef4593, undef4597, undef4974, undef4979, undef4988, undef4989, undef4996, undef5001, undef5188, undef5472, undef5596, undef5669, undef5819, undef5820, undef5821, undef5826, undef5834, undef5837, undef5856, undef5857, undef5858, undef5859, undef5863, undef5871, undef5877, undef5878, undef5884, undef5885, Undef variables: undef34, undef51, undef59, undef60, undef61, undef78, undef185, undef769, undef775, undef790, undef1907, undef2137, undef2609, undef2994, undef3991, undef4108, undef4573, undef4582, undef4592, undef4593, undef4597, undef4974, undef4979, undef4988, undef4989, undef4996, undef5001, undef5188, undef5472, undef5596, undef5669, undef5819, undef5820, undef5821, undef5826, undef5834, undef5837, undef5856, undef5857, undef5858, undef5859, undef5863, undef5871, undef5877, undef5878, undef5884, undef5885, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: (~(1) + i^0)}> (0 + ap_listeners^0), status^0 -> undef4582}> (0 + ap_listeners^0), status^0 -> undef4582}> (0 + undef2609), lr^0 -> (0 + ap_listeners^0), status^0 -> undef4582}> (1 + requests_this_child^0)}> (1 + requests_this_child^0)}> (0 + ap_listeners^0), requests_this_child^0 -> (1 + requests_this_child^0), status^0 -> undef4582}> (0 + ap_listeners^0), requests_this_child^0 -> (1 + requests_this_child^0), status^0 -> undef4582}> (0 + undef2609), lr^0 -> (0 + ap_listeners^0), requests_this_child^0 -> (1 + requests_this_child^0), status^0 -> undef4582}> (1 + requests_this_child^0)}> (1 + requests_this_child^0)}> (0 + ap_listeners^0), requests_this_child^0 -> (1 + requests_this_child^0), status^0 -> undef4582}> (0 + ap_listeners^0), requests_this_child^0 -> (1 + requests_this_child^0), status^0 -> undef4582}> (0 + undef2609), lr^0 -> (0 + ap_listeners^0), requests_this_child^0 -> (1 + requests_this_child^0), status^0 -> undef4582}> 1, status^0 -> undef4582}> 1, status^0 -> undef4582}> (0 + undef2609), lr^0 -> 1, status^0 -> undef4582}> 0, lr^0 -> 1, status^0 -> undef4582}> 0, lr^0 -> 1, status^0 -> undef4582}> (0 + undef2609), last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582}> 1, status^0 -> undef4582}> 1, status^0 -> undef4582}> (0 + undef2609), lr^0 -> 1, status^0 -> undef4582}> 0, lr^0 -> 1, status^0 -> undef4582}> 0, lr^0 -> 1, status^0 -> undef4582}> (0 + undef2609), last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582}> (0 + undef775)}> (0 + undef775)}> (0 + undef775)}> 1, status^0 -> undef4582}> 1, status^0 -> undef4582}> (0 + undef2609), lr^0 -> 1, status^0 -> undef4582}> 0, lr^0 -> 1, status^0 -> undef4582}> 0, lr^0 -> 1, status^0 -> undef4582}> (0 + undef2609), last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582}> (0 + undef775)}> (0 + undef775)}> (0 + undef775)}> 1}> 1}> 1}> 1}> (0 + undef2609)}> Fresh variables: undef34, undef51, undef59, undef60, undef61, undef78, undef185, undef769, undef775, undef790, undef1907, undef2137, undef2609, undef2994, undef3991, undef4108, undef4573, undef4582, undef4592, undef4593, undef4597, undef4974, undef4979, undef4988, undef4989, undef4996, undef5001, undef5188, undef5472, undef5596, undef5669, undef5819, undef5820, undef5821, undef5826, undef5834, undef5837, undef5856, undef5857, undef5858, undef5859, undef5863, undef5871, undef5877, undef5878, undef5884, undef5885, Undef variables: undef34, undef51, undef59, undef60, undef61, undef78, undef185, undef769, undef775, undef790, undef1907, undef2137, undef2609, undef2994, undef3991, undef4108, undef4573, undef4582, undef4592, undef4593, undef4597, undef4974, undef4979, undef4988, undef4989, undef4996, undef5001, undef5188, undef5472, undef5596, undef5669, undef5819, undef5820, undef5821, undef5826, undef5834, undef5837, undef5856, undef5857, undef5858, undef5859, undef5863, undef5871, undef5877, undef5878, undef5884, undef5885, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: -1 + i^0, rest remain the same}> Variables: i^0 Graph 2: Transitions: ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> undef2609, rest remain the same}> Variables: ap_max_requests_per_child^0, die_now^0, num_listensocks^0, ap_listeners^0, lr^0, status^0, current_conn^0, requests_this_child^0, last_poll_idx^0, numdesc___05^0, one_process^0, shutdown_pending^0, ap_my_generation^0 Graph 3: Transitions: Variables: Graph 4: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 Graph 3 Graph 4 undef775, rest remain the same}> undef775, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 1 ) ( 6 , 2 ) ( 8 , 2 ) ( 10 , 4 ) ( 18 , 3 ) ( 21 , 2 ) ( 23 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.002061 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001834s Ranking function: -1 + i^0 New Graphs: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.29304 Checking conditional termination of SCC {l6, l8, l21, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.041339s Ranking function: -24 + 6*ap_max_requests_per_child^0 + 9*num_listensocks^0 - 6*requests_this_child^0 New Graphs: Transitions: ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> undef2609, rest remain the same}> Variables: ap_listeners^0, ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l21, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.028839s Ranking function: -22 + 22*ap_max_requests_per_child^0 - 9*num_listensocks^0 - 22*requests_this_child^0 New Graphs: Transitions: ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> undef2609, rest remain the same}> Variables: ap_listeners^0, ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l21, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.027485s Ranking function: -22 + 24*ap_max_requests_per_child^0 - 2*num_listensocks^0 - 24*requests_this_child^0 New Graphs: Transitions: ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> 1, rest remain the same}> undef2609, rest remain the same}> Variables: ap_listeners^0, ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l21, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.018856s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.355308s Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.116847s Time used: 0.114523 Trying to remove transition: 1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.054586s Time used: 0.052619 Trying to remove transition: 1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.055565s Time used: 0.053582 Trying to remove transition: 1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.059161s Time used: 0.057246 Trying to remove transition: 1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.055069s Time used: 0.053169 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.060528s Time used: 0.058695 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.046024s Time used: 0.044205 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.076966s Time used: 0.075314 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.082301s Time used: 0.07988 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.100966s Time used: 0.098718 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.081274s Time used: 0.078899 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.070383s Time used: 0.067909 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.071181s Time used: 0.068839 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.082848s Time used: 0.080549 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.062778s Time used: 0.060617 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.080357s Time used: 0.07852 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.074927s Time used: 0.072461 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.079891s Time used: 0.077494 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.093186s Time used: 0.090862 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.072115s Time used: 0.069529 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.073624s Time used: 0.071406 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.097583s Time used: 0.09538 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.070474s Time used: 0.06793 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.112117s Time used: 0.109832 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.097836s Time used: 0.095476 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.072794s Time used: 0.070111 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.091981s Time used: 0.089756 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.294547s Time used: 0.292253 Trying to remove transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.116245s Time used: 0.11245 Trying to remove transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.161003s Time used: 0.157666 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.089474s Time used: 0.086025 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.088327s Time used: 0.085815 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.136586s Time used: 0.134125 Trying to remove transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.093714s Time used: 0.090556 Trying to remove transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.111897s Time used: 0.109031 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.539648s Time used: 1.53663 LOG: SAT solveNonLinear - Elapsed time: 1.539648s Cost: 0; Total time: 1.53663 Termination implied by a set of invariant(s): Invariant at l8: die_now^0 <= 0 Invariant at l21: die_now^0 <= 0 Invariant at l23: die_now^0 <= 0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): Ranking function: -die_now^0 New Graphs: Transitions: ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> undef2609, rest remain the same}> undef2609, rest remain the same}> Variables: ap_listeners^0, ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.033206s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.561095s Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.217105s Time used: 0.212883 Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.280459s Time used: 0.276726 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.093701s Time used: 0.089965 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.091470s Time used: 0.088137 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.150012s Time used: 0.147193 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.130139s Time used: 0.126395 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.103994s Time used: 0.100375 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.104703s Time used: 0.101692 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.154672s Time used: 0.151664 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.161516s Time used: 0.157784 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.127879s Time used: 0.124046 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.125585s Time used: 0.122216 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.106094s Time used: 0.103171 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.091083s Time used: 0.088413 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.166072s Time used: 0.163597 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.183065s Time used: 0.179217 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.105890s Time used: 0.102064 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.109550s Time used: 0.106572 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.149907s Time used: 0.146904 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.173697s Time used: 0.169967 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.110316s Time used: 0.106238 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.142073s Time used: 0.138779 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.332633s Time used: 0.329636 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.167816s Time used: 0.16397 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.108206s Time used: 0.104308 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.142294s Time used: 0.138817 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.149671s Time used: 0.146612 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.144562s Time used: 0.140904 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.110206s Time used: 0.106407 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.133153s Time used: 0.129855 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.511969s Time used: 0.50887 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.419614s Time used: 0.41493 Trying to remove transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.163073s Time used: 0.158237 Trying to remove transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.200689s Time used: 0.196654 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.193351s Time used: 0.189177 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.271195s Time used: 0.267964 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.193138s Time used: 0.189942 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.173769s Time used: 0.169541 Trying to remove transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.138030s Time used: 0.133773 Trying to remove transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.183048s Time used: 0.17977 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 3.544282s Time used: 3.53542 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.469907s Time used: 0.469894 LOG: SAT solveNonLinear - Elapsed time: 4.014189s Cost: 1; Total time: 4.00531 Failed at location 6: 1 <= die_now^0 Before Improving: Quasi-invariant at l6: 1 <= die_now^0 Quasi-invariant at l8: 1 <= die_now^0 Quasi-invariant at l21: 1 <= die_now^0 Quasi-invariant at l23: 1 <= die_now^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.095815s Remaining time after improvement: 0.938915 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l6: 1 <= die_now^0 Quasi-invariant at l8: 1 <= die_now^0 Quasi-invariant at l21: 1 <= die_now^0 Quasi-invariant at l23: 1 <= die_now^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: New Graphs: INVARIANTS: 8: die_now^0 <= 0 , 21: die_now^0 <= 0 , 23: die_now^0 <= 0 , Quasi-INVARIANTS to narrow Graph: 8: 21: 23: Calling Safety with literal 1 <= die_now^0 and entry LOG: CALL check - Post:1 <= die_now^0 - Process 1 * Exit transition: * Postcondition : 1 <= die_now^0 Postcodition moved up: 1 <= die_now^0 LOG: Try proving POST Postcondition: 1 <= die_now^0 LOG: CALL check - Post:1 <= die_now^0 - Process 2 * Exit transition: * Postcondition : 1 <= die_now^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005446s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.005571s Postcondition: 1 <= die_now^0 LOG: CALL check - Post:1 <= die_now^0 - Process 3 * Exit transition: * Postcondition : 1 <= die_now^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005597s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.005715s Postcondition: 1 <= die_now^0 LOG: CALL check - Post:1 <= die_now^0 - Process 4 * Exit transition: * Postcondition : 1 <= die_now^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005415s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.005525s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 Narrowing transition: -1 + i^0, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: END ENTRIES: GRAPH: -1 + i^0, rest remain the same}> END GRAPH: EXIT: POST: 1 <= die_now^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.020339s Time used: 4.01995 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.016094s Time used: 4.01293 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.015686s Time used: 1.01315 LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 9.151823s INVARIANTS: 6: 8: 21: 23: Quasi-INVARIANTS to narrow Graph: 6: 1 <= die_now^0 , 8: 1 <= die_now^0 , 21: 1 <= die_now^0 , 23: 1 <= die_now^0 , Narrowing transition: LOG: Narrow transition size 1 Narrowing transition: LOG: Narrow transition size 1 Narrowing transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + requests_this_child^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + requests_this_child^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + requests_this_child^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + requests_this_child^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef775, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef775, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef775, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef775, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: LOG: Narrow transition size 1 It's unfeasible. Removing transition: 1, rest remain the same}> It's unfeasible. Removing transition: 1, rest remain the same}> Narrowing transition: LOG: Narrow transition size 1 It's unfeasible. Removing transition: 1, rest remain the same}> It's unfeasible. Removing transition: 1, rest remain the same}> Narrowing transition: undef2609, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: LOG: Narrow transition size 1 Narrowing transition: LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> undef2609, rest remain the same}> Variables: ap_max_requests_per_child^0, die_now^0, num_listensocks^0, ap_listeners^0, lr^0, status^0, current_conn^0, requests_this_child^0, last_poll_idx^0, numdesc___05^0, one_process^0, shutdown_pending^0, ap_my_generation^0 Checking conditional termination of SCC {l6, l8, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.059517s Ranking function: -24 + 6*ap_max_requests_per_child^0 + 9*num_listensocks^0 - 6*requests_this_child^0 New Graphs: Transitions: ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> undef2609, rest remain the same}> undef2609, rest remain the same}> Variables: ap_listeners^0, ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.059468s Ranking function: -22 + 22*ap_max_requests_per_child^0 - 9*num_listensocks^0 - 4*requests_this_child^0 New Graphs: Transitions: ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> undef2609, rest remain the same}> undef2609, rest remain the same}> Variables: ap_listeners^0, ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.059358s Ranking function: -22 + 24*ap_max_requests_per_child^0 - 2*num_listensocks^0 - 24*requests_this_child^0 New Graphs: Transitions: ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> undef2609, rest remain the same}> undef2609, rest remain the same}> Variables: ap_listeners^0, ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.034924s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.554146s Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.222650s Time used: 0.218935 Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.286882s Time used: 0.283793 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.100308s Time used: 0.097155 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.088180s Time used: 0.085321 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.156812s Time used: 0.154111 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.138386s Time used: 0.134596 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.112357s Time used: 0.108662 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.112806s Time used: 0.109677 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.162261s Time used: 0.15925 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.170358s Time used: 0.166566 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.135084s Time used: 0.131215 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.132874s Time used: 0.129756 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.114355s Time used: 0.111359 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.099091s Time used: 0.096386 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.174258s Time used: 0.171695 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.191180s Time used: 0.187389 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.114960s Time used: 0.111081 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.117941s Time used: 0.115035 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.158653s Time used: 0.155695 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.183497s Time used: 0.179687 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.118529s Time used: 0.114682 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.150880s Time used: 0.147599 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.339421s Time used: 0.336452 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.176436s Time used: 0.172602 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.116949s Time used: 0.113056 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.150923s Time used: 0.147895 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.158410s Time used: 0.155321 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.153446s Time used: 0.149766 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.118744s Time used: 0.115015 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.141919s Time used: 0.138811 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.520724s Time used: 0.517698 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.427029s Time used: 0.422415 Trying to remove transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.171257s Time used: 0.166443 Trying to remove transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.208422s Time used: 0.204577 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.199489s Time used: 0.195355 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.277281s Time used: 0.273861 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.200741s Time used: 0.197319 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.181648s Time used: 0.177494 Trying to remove transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.131344s Time used: 0.127127 Trying to remove transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.190588s Time used: 0.187334 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 3.132362s Time used: 3.12404 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.880981s Time used: 0.880949 LOG: SAT solveNonLinear - Elapsed time: 4.013342s Cost: 1; Total time: 4.00499 Failed at location 6: 1 <= ap_max_requests_per_child^0 + die_now^0 Before Improving: Quasi-invariant at l6: 1 <= ap_max_requests_per_child^0 + die_now^0 Quasi-invariant at l8: 1 <= ap_max_requests_per_child^0 + die_now^0 Quasi-invariant at l21: 1 <= ap_max_requests_per_child^0 + die_now^0 Quasi-invariant at l23: 1 <= ap_max_requests_per_child^0 + die_now^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.086303s Remaining time after improvement: 0.94747 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l6: 1 <= ap_max_requests_per_child^0 + die_now^0 Quasi-invariant at l8: 1 <= ap_max_requests_per_child^0 + die_now^0 Quasi-invariant at l21: 1 <= ap_max_requests_per_child^0 + die_now^0 Quasi-invariant at l23: 1 <= ap_max_requests_per_child^0 + die_now^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): New Graphs: Transitions: 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> undef2609, rest remain the same}> undef2609, rest remain the same}> Variables: ap_listeners^0, ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.032724s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.593617s Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.322453s Time used: 0.317522 Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.398708s Time used: 0.395192 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.129815s Time used: 0.126081 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.109660s Time used: 0.106367 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.187431s Time used: 0.184645 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.194045s Time used: 0.189284 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.134276s Time used: 0.130384 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.155850s Time used: 0.152035 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.176966s Time used: 0.173791 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.207268s Time used: 0.203512 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.146253s Time used: 0.142368 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.160637s Time used: 0.157008 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.132932s Time used: 0.129692 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.144632s Time used: 0.141775 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.192297s Time used: 0.189639 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.188283s Time used: 0.184592 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.131761s Time used: 0.127892 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.169285s Time used: 0.166272 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.195142s Time used: 0.191976 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.203492s Time used: 0.199705 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.153149s Time used: 0.149283 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.153321s Time used: 0.149857 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.195343s Time used: 0.192188 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.163252s Time used: 0.159291 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.131429s Time used: 0.127772 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.151120s Time used: 0.147996 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.171656s Time used: 0.168626 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.193513s Time used: 0.188787 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.188201s Time used: 0.184451 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.173905s Time used: 0.170335 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.398904s Time used: 0.395744 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.567145s Time used: 0.562804 Trying to remove transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.450495s Time used: 0.446045 Trying to remove transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.433523s Time used: 0.429612 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.184273s Time used: 0.18041 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.218222s Time used: 0.215437 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003583s Time used: 4.00023 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.020816s Time used: 4.00021 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.900670s Time used: 1.85113 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.922504s Time used: 2.83685 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.005512s Time used: 1.00548 LOG: SAT solveNonLinear - Elapsed time: 3.928016s Cost: 1; Total time: 3.84234 Termination implied by a set of invariant(s): Invariant at l21: 1 <= status^0 Invariant at l23: 1 <= ap_max_requests_per_child^0 + die_now^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): Quasi-ranking function: 50000 + 2*ap_max_requests_per_child^0 - requests_this_child^0 New Graphs: Transitions: 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> undef2609, rest remain the same}> undef2609, rest remain the same}> Variables: ap_listeners^0, ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.038025s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.649564s Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.358395s Time used: 0.353297 Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.334958s Time used: 0.331019 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.140696s Time used: 0.136838 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.127281s Time used: 0.123807 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.216868s Time used: 0.21376 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.216538s Time used: 0.211288 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.157175s Time used: 0.152675 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.178810s Time used: 0.174704 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.270781s Time used: 0.266743 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.223804s Time used: 0.218954 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.174488s Time used: 0.170315 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.183498s Time used: 0.179627 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.249470s Time used: 0.246119 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.134998s Time used: 0.131773 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.222253s Time used: 0.219671 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.228220s Time used: 0.224469 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.162148s Time used: 0.158307 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.174150s Time used: 0.170821 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.234612s Time used: 0.231465 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.233572s Time used: 0.22955 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.177850s Time used: 0.173924 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.196497s Time used: 0.192975 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.189114s Time used: 0.185922 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.186941s Time used: 0.183222 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.156166s Time used: 0.152418 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.178921s Time used: 0.175551 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.194077s Time used: 0.191044 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.191582s Time used: 0.187998 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.179195s Time used: 0.175579 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.184850s Time used: 0.181355 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.294413s Time used: 0.291339 Trying to remove transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.623175s Time used: 0.618947 Trying to remove transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.265370s Time used: 0.260851 Trying to remove transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.193588s Time used: 0.190008 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.140543s Time used: 0.137164 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.142585s Time used: 0.140012 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 3.654936s Time used: 3.64823 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.357575s Time used: 0.35757 LOG: SAT solveNonLinear - Elapsed time: 4.012512s Cost: 1; Total time: 4.0058 Failed at location 6: 1 + ap_max_requests_per_child^0 <= die_now^0 + num_listensocks^0 Before Improving: Quasi-invariant at l6: 1 + ap_max_requests_per_child^0 <= die_now^0 + num_listensocks^0 Quasi-invariant at l8: 1 + ap_max_requests_per_child^0 <= die_now^0 + num_listensocks^0 Quasi-invariant at l21: 1 + ap_max_requests_per_child^0 <= die_now^0 + num_listensocks^0 Quasi-invariant at l23: 1 + ap_max_requests_per_child^0 <= die_now^0 + num_listensocks^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.085698s Remaining time after improvement: 0.944089 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l6: 1 + ap_max_requests_per_child^0 <= die_now^0 + num_listensocks^0 Quasi-invariant at l8: 1 + ap_max_requests_per_child^0 <= die_now^0 + num_listensocks^0 Quasi-invariant at l21: 1 + ap_max_requests_per_child^0 <= die_now^0 + num_listensocks^0 Quasi-invariant at l23: 1 + ap_max_requests_per_child^0 <= die_now^0 + num_listensocks^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + requests_this_child^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> ((0 + 1) + 0) + requests_this_child^0, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): New Graphs: Transitions: 1 + requests_this_child^0, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> undef2609, rest remain the same}> undef2609, rest remain the same}> Variables: ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.034263s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.540508s Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.384947s Time used: 0.380863 Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.453548s Time used: 0.449731 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.315454s Time used: 0.311916 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.227911s Time used: 0.224479 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.280655s Time used: 0.27743 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.455341s Time used: 0.451361 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.373640s Time used: 0.369708 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.240531s Time used: 0.23702 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.466972s Time used: 0.463499 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.394732s Time used: 0.390908 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.293541s Time used: 0.289604 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.412867s Time used: 0.40947 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.219485s Time used: 0.216182 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.209276s Time used: 0.206356 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.252860s Time used: 0.250283 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.275994s Time used: 0.272225 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.359335s Time used: 0.355468 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.352918s Time used: 0.349608 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.404086s Time used: 0.400808 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.728008s Time used: 0.724013 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.405885s Time used: 0.401841 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.319785s Time used: 0.316368 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.256105s Time used: 0.252934 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.487734s Time used: 0.483837 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.287897s Time used: 0.28402 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.219856s Time used: 0.216314 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.259797s Time used: 0.256568 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.390592s Time used: 0.386916 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.250728s Time used: 0.246948 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.314288s Time used: 0.31071 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.193173s Time used: 0.189981 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002965s Time used: 4 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.017515s Time used: 4.00033 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.551611s Time used: 1.51238 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.195791s Time used: 2.12626 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.006162s Time used: 1.00613 LOG: SAT solveNonLinear - Elapsed time: 3.201952s Cost: 1; Total time: 3.13239 Termination implied by a set of invariant(s): Invariant at l8: 1 <= ap_max_requests_per_child^0 Invariant at l21: 0 <= die_now^0 + num_listensocks^0 Invariant at l23: lr^0 <= ap_max_requests_per_child^0 + die_now^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): Quasi-ranking function: 50000 + ap_max_requests_per_child^0 + die_now^0 + num_listensocks^0 - requests_this_child^0 New Graphs: Transitions: 1 + requests_this_child^0, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> undef2609, rest remain the same}> undef2609, rest remain the same}> Variables: ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.038696s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.724334s Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.521987s Time used: 0.51682 Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.595916s Time used: 0.59155 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.223920s Time used: 0.219695 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.207197s Time used: 0.203533 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.498781s Time used: 0.495313 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.545614s Time used: 0.540924 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.421529s Time used: 0.416584 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.436313s Time used: 0.432227 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.282811s Time used: 0.279327 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.402117s Time used: 0.397978 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.352729s Time used: 0.348727 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.414765s Time used: 0.411243 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.225210s Time used: 0.221807 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.225130s Time used: 0.222108 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.745876s Time used: 0.742994 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.523341s Time used: 0.519416 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.298392s Time used: 0.294481 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.361952s Time used: 0.358642 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.634003s Time used: 0.630525 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.602816s Time used: 0.598863 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.350660s Time used: 0.34672 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.269538s Time used: 0.266038 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.295314s Time used: 0.291966 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.617239s Time used: 0.613394 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.230095s Time used: 0.226062 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.354210s Time used: 0.350852 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.426863s Time used: 0.42349 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.305800s Time used: 0.301859 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.496256s Time used: 0.492375 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.322143s Time used: 0.31856 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.208419s Time used: 0.205237 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003345s Time used: 4.00035 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.017031s Time used: 4.00001 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.621763s Time used: 1.58393 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.977301s Time used: 1.90756 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.007068s Time used: 1.00694 LOG: SAT solveNonLinear - Elapsed time: 2.984369s Cost: 1; Total time: 2.9145 Termination implied by a set of invariant(s): Invariant at l8: 1 + ap_max_requests_per_child^0 <= num_listensocks^0 Invariant at l21: lr^0 <= die_now^0 + num_listensocks^0 + status^0 Invariant at l23: 1 <= ap_max_requests_per_child^0 + die_now^0 + lr^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef775, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef2609, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): Quasi-ranking function: 50000 + ap_max_requests_per_child^0 - die_now^0 + num_listensocks^0 - requests_this_child^0 New Graphs: Transitions: 1 + requests_this_child^0, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> undef2609, rest remain the same}> undef2609, rest remain the same}> Variables: ap_max_requests_per_child^0, ap_my_generation^0, current_conn^0, die_now^0, last_poll_idx^0, lr^0, num_listensocks^0, numdesc___05^0, one_process^0, requests_this_child^0, shutdown_pending^0, status^0 Checking conditional termination of SCC {l6, l8, l23}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.043619s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.632447s Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.641364s Time used: 0.635704 Trying to remove transition: undef2609, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.493295s Time used: 0.488891 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.263107s Time used: 0.25892 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.226397s Time used: 0.222655 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.325166s Time used: 0.321848 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.510105s Time used: 0.505665 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.393191s Time used: 0.388016 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.366415s Time used: 0.362672 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.494019s Time used: 0.490451 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.502020s Time used: 0.497952 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.318608s Time used: 0.314383 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.317341s Time used: 0.313578 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.200502s Time used: 0.196897 Trying to remove transition: undef775, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.221021s Time used: 0.218272 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.374379s Time used: 0.37164 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.251310s Time used: 0.247542 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.368781s Time used: 0.365214 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.358827s Time used: 0.355301 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.230681s Time used: 0.227402 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.557787s Time used: 0.554418 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.266678s Time used: 0.262737 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.256360s Time used: 0.252941 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.494648s Time used: 0.491425 Trying to remove transition: undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.231938s Time used: 0.228054 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.335543s Time used: 0.332091 Trying to remove transition: 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.241779s Time used: 0.238253 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.230806s Time used: 0.227694 Trying to remove transition: undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.540573s Time used: 0.53716 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.312664s Time used: 0.308649 Trying to remove transition: 1, status^0 -> undef4582, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.411705s Time used: 0.408314 Trying to remove transition: 1 + requests_this_child^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.263687s Time used: 0.260441 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.462080s Time used: 0.459301 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.934132s Time used: 0.918412 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.704638s Time used: 1.66839 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.912829s Time used: 0.84663 Proving non-termination of subgraph 2 Transitions: ap_listeners^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> 1 + requests_this_child^0, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> ap_listeners^0, requests_this_child^0 -> 1 + requests_this_child^0, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> 1, status^0 -> undef4582, rest remain the same}> undef2609, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef2609, last_poll_idx^0 -> 0, lr^0 -> 1, status^0 -> undef4582, rest remain the same}> undef775, rest remain the same}> undef775, rest remain the same}> undef2609, rest remain the same}> Variables: ap_max_requests_per_child^0, die_now^0, num_listensocks^0, ap_listeners^0, lr^0, status^0, current_conn^0, requests_this_child^0, last_poll_idx^0, numdesc___05^0, one_process^0, shutdown_pending^0, ap_my_generation^0 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.149634s Checking conditional non-termination of SCC {l6, l8, l21, l23}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.003437s Time used: 5.00046 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.092244s Time used: 5.00118 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 7.753885s Time used: 7.6127 > Checking if the negation of the conditions of every pending exit is quasi-invariant... YES Calling reachability with... Transition: Conditions: die_now^0 <= 0, OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: die_now^0 <= 0, OPEN EXITS: (condsUp: die_now^0 <= 0) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: i^0 <= 0, die_now^0 <= 0, Transition: Conditions: i^0 <= 0, die_now^0 <= 0, Transition: Conditions: i^0 <= 0, die_now^0 <= 0, OPEN EXITS: > Conditions are not feasible after transitions. --- Reachability graph --- Transitions: -1 + i^0, rest remain the same}> Variables: i^0 Checking edge-closing of SCC {l2}... > No exit transition to close. Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.065620s Ranking function: -1 + i^0 New Graphs: Calling reachability with... Transition: Conditions: die_now^0 <= 0, Transition: Conditions: die_now^0 <= 0, Transition: Conditions: die_now^0 <= 0, OPEN EXITS: > Conditions are reachable! Program does NOT terminate