NAME: bug4.c
CITE: \cite{LLNL:Pthreads:URL}
TYPE: $\text{P}$
SCALE: {\texttt{NT=3, ITR=5, THD=7, NSTEPS=10}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (93.6 files/s, 11892.5 lines/s)"
1,C,15,27,85
civl verify -enablePrintf=false -inputITERATIONS=5 -inputTHRESHOLD=7 -inputNSTEPS=10 llnl/bug4.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 494:
CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
at pthread.cvl:761.2-7 "$wait":
A deadlock is possible:
  Path condition: (0 <= -1*X0+9) && (0 <= X0+-1)
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): terminated
process p3 (id=3): terminated

Call stacks:

process p0 (id=0):
  pthread_join at pthread.cvl:761.2-7 "$wait" called from
  _gen_main at bug4.c:115.4-16 "pthread_join" called from
  _CIVL_system at GeneralTransformer:0.-1-20 "_gen_argc, &_gen_a..." inserted by GeneralTransformer.new main function before bug4.c:95.13-17 "argc"

process p1 (id=1):
  $pthread_cond_wait at pthread.cvl:998.4-16 "cond->signal" called from
  sub1 at bug4.c:52.2-19 "pthread_cond_wait"

process p2 (id=2):
  terminated

process p3 (id=3):
  terminated

Logging new entry 0, writing trace to CIVLREP/bug4_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -inputITERATIONS=5 -inputTHRESHOLD=7 -inputNSTEPS=10 llnl/bug4.c 

=== Stats ===
   time (s)            : 4.44
   memory (bytes)      : 650117120
   max process count   : 4
   states              : 12162
   states saved        : 5698
   state matches       : 436
   transitions         : 12597
   trace steps         : 6132
   valid calls         : 37915
   provers             : z3, cvc4, cvc3
   prover calls        : 3

=== Result ===
The program MAY NOT be correct.  See CIVLREP/bug4_log.txt
NAME: queue{\U}ok{\U}longest{\U}...c
CITE: \cite{svcomp:2015} 
TYPE: $\text{P}$
SCALE: {\texttt{SIZE=800}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (92.5 files/s, 14054.7 lines/s)"
1,C,26,0,126
civl verify -enablePrintf=false -svcomp -inputSIZE=800 -inputEMPTY=-1 -inputFULL=-2 queue_ok_longest_true-unreach-call.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
17s: mem=803Mb trans=71168 traceSteps=47995 explored=67977 saved=44805 prove=2

=== Command ===
civl verify -enablePrintf=false -svcomp -inputSIZE=800 -inputEMPTY=-1 -inputFULL=-2 queue_ok_longest_true-unreach-call.c 

=== Stats ===
   time (s)            : 16.47
   memory (bytes)      : 842530816
   max process count   : 3
   states              : 68364
   states saved        : 44979
   state matches       : 3211
   transitions         : 71574
   trace steps         : 48189
   valid calls         : 121365
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
NAME: read{\U}write{\U}lock{\U}...c
CITE: \cite{svcomp:2015} 
TYPE: $\text{P}$
SCALE: {\texttt{NT=4}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (103.2 files/s, 5572.7 lines/s)"
1,C,10,6,38
civl verify -enablePrintf=false -svcomp read_write_lock_false-unreach-call.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 59:
CIVL execution violation in p2(id=1) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before read_write_lock_false-unreach-call.c:42.0-3 "int":


Context: true

Assertion: $assert(false)
-> false

Call stacks:

process p0 (id=0):
  pthread_join at pthread.cvl:761.2-7 "$wait" called from
  _CIVL_system at read_write_lock_false-unreach-call.c:51.2-14 "pthread_join"

process p2 (id=1):
  reader at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before read_write_lock_false-unreach-call.c:42.0-3 "int"

Logging new entry 0, writing trace to CIVLREP/read_write_lock_false-unreach-call_0.trace
Terminating search after finding 1 violation.

=== Command ===
civl verify -enablePrintf=false -svcomp read_write_lock_false-unreach-call.c 

=== Stats ===
   time (s)            : 1.7
   memory (bytes)      : 514850816
   max process count   : 5
   states              : 1758
   states saved        : 1105
   state matches       : 119
   transitions         : 1878
   trace steps         : 1223
   valid calls         : 1762
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/read_write_lock_false-unreach-call_log.txt
NAME: sync01{\U}true...c
CITE: \cite{svcomp:2015} 
TYPE: $\text{P}$
SCALE: {\texttt{NT=2}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (103.8 files/s, 6851.6 lines/s)"
1,C,24,0,42
civl verify -enablePrintf=false -svcomp sync01_true-unreach-call.c
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp sync01_true-unreach-call.c 

=== Stats ===
   time (s)            : 1.49
   memory (bytes)      : 514850816
   max process count   : 3
   states              : 320
   states saved        : 178
   state matches       : 10
   transitions         : 329
   trace steps         : 187
   valid calls         : 602
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
NAME: 03{\U}incdec{\U}true...c
CITE: \cite{svcomp:2015} 
TYPE: $\text{P}$
SCALE: {\texttt{NT=3}}

files,language,blank,comment,code,"http://cloc.sourceforge.net v 1.62  T=0.01 s (97.2 files/s, 8067.7 lines/s)"
1,C,24,3,56
civl verify -enablePrintf=false -svcomp -procBound=3 03_incdec_true-unreach-call.c	
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp -procBound=3 03_incdec_true-unreach-call.c 

=== Stats ===
   time (s)            : 1.31
   memory (bytes)      : 514850816
   max process count   : 3
   states              : 448
   states saved        : 188
   state matches       : 6
   transitions         : 453
   trace steps         : 191
   valid calls         : 116
   provers             : z3, cvc4, cvc3
   prover calls        : 3

=== Result ===
The standard properties hold for all executions.
