COPPER version 2.0 ...
Command Line: copper --default --specification abs_2 philosopher.pp philosopher.spec --trace 
Simplify process started ...
parsing preprocessed C file philosopher.pp ...
parsing specification file philosopher.spec ...
control locations created ...
skip locations eliminated ...
useless branch locations eliminated ...
procedures inlined ...
number of locations before parallelization = 10 ...
number of locations after parallelization = 9 ...
proc manager for philosopher created ...
component for philosopher created ...
relevant propositions computed ...
inputs processed ...
checking PhilSpec2 {trace} temp_var_8
starting iteration number 1 ...
model extracted in 0.2 milliseconds ...
implementation machine extracted in 0.5 milliseconds ...
global states : ( 1048576 ) = 1048576
[<<-1>> {P0::eating = 0} <<[]>>:65535:255]
#################################################
=================================================
+++++++++++++++++++++++++++++++++++++++++++++++++
		P0::epsilon
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> branch ( 1 ) <<[]>>:65535:255]
#################################################
=================================================
+++++++++++++++++++++++++++++++++++++++++++++++++
		P0::epsilon
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> P0::temp_var_10 = pick_left (  ) <<[]>>:65535:255]
#################################################
=================================================
+++++++++++++++++++++++++++++++++++++++++++++++++
		P0::epsilon
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> P0::temp_var_10 = pick_left (  ) <<[]>>:0:0]
#################################################
=================================================
+++++++++++++++++++++++++++++++++++++++++++++++++
		pick_left
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> P0::temp_var_10 = pick_left (  ) <<[]>>:0:2]
#################################################
=================================================
+++++++++++++++++++++++++++++++++++++++++++++++++
		P0::epsilon
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> P0::temp_var_11 = __COPPER_HANDSHAKE__ ( "pick_right"  ) <<[]>>:65535:255]
#################################################
=================================================
+++++++++++++++++++++++++++++++++++++++++++++++++
		pick_right
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> P0::temp_var_11 = __COPPER_HANDSHAKE__ ( "pick_right"  ) <<[]>>:0:0]
#################################################
=================================================
reachability checked in 8.0 milliseconds ...
Cprover formula has 220 variables and 551 clauses ...
Cprover formula has 315 variables and 685 clauses ...
<<< BEGIN CONCRETE COUNTEREXAMPLE >>>
[<<-1>> {P0::eating = 0} <<[]>>:65535:255]
#################################################
=================================================

+++++++++++++++++++++++++++++++++++++++++++++++++
		P0::epsilon
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> branch ( 1 ) <<[]>>:65535:255]
#################################################
=================================================
(P0::eating = 0)
+++++++++++++++++++++++++++++++++++++++++++++++++
		P0::epsilon
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> P0::temp_var_10 = pick_left (  ) <<[]>>:65535:255]
#################################################
=================================================
(P0::eating = 0)
+++++++++++++++++++++++++++++++++++++++++++++++++
		P0::epsilon
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> P0::temp_var_10 = pick_left (  ) <<[]>>:0:0]
#################################################
=================================================
(P0::eating = 0)
+++++++++++++++++++++++++++++++++++++++++++++++++
		pick_left
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> P0::temp_var_10 = pick_left (  ) <<[]>>:0:2]
#################################################
=================================================
(P0::eating = 0)
+++++++++++++++++++++++++++++++++++++++++++++++++
		P0::epsilon
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> P0::temp_var_11 = __COPPER_HANDSHAKE__ ( "pick_right"  ) <<[]>>:65535:255]
#################################################
=================================================
(P0::eating = 0)
+++++++++++++++++++++++++++++++++++++++++++++++++
		pick_right
+++++++++++++++++++++++++++++++++++++++++++++++++
[<<-1>> P0::temp_var_11 = __COPPER_HANDSHAKE__ ( "pick_right"  ) <<[]>>:0:0]
#################################################
=================================================
(P0::eating = 0)
<<< END CONCRETE COUNTEREXAMPLE >>>
conformance relation does not exist !!
specification abs_2 is invalid ...
total global time = 57.5 milliseconds
total cpu time = 20.0 milliseconds
total input processing time = 13.2 milliseconds
total Buchi automaton construction time = 0.0 milliseconds
total implementation machine extraction time = 0.5 milliseconds
total verification time = 8.0 milliseconds
total proof generation time = 0.0 milliseconds
total abstraction refinement time = 30.6 milliseconds
total CE generation time = 6.3 milliseconds
total CE verification time = 0.0 milliseconds
total predicate abstraction refinement time = 0.0 milliseconds
total LTS abstraction refinement time = 0.0 milliseconds
total number of eliminating combinations = 0
max number of eliminating combinations for a CE = 0
max size of eliminating combination = 0
max size of tried combination = 0
number of iterations = 1
number of predicate iterations = 1
number of lts iterations = 0
number of seed branches : 0
number of explored states : 1048576
number of theorem prover calls = 2
number of formulas found in cache = 0
number of formulas stored in cache = 2
number of membership calls to MAT = 0
number of MAT membership cache misses = 0
number of candidate calls to MAT = 0
assumption alphabet size = 0
optimal assumption alphabet size = 0
assumption alphabet ratio = 0.000000
total certificate CNF size = 0
total certificate resolution file size = 0
total certificate packed resolution file size = 0
total certificate zipped resolution file size = 0
total witness file size = 0
total witness zipped file size = 0
total certificate zipped file size = 0
Simplify process destroyed ...
terminating normally ...