civl verify -enablePrintf=false -svcomp dekker_true.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp dekker_true.c 

=== Stats ===
   time (s)            : 1.57
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 235
   states saved        : 174
   state matches       : 45
   transitions         : 279
   trace steps         : 218
   valid calls         : 129
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp lamport_true.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp lamport_true.c 

=== Stats ===
   time (s)            : 1.77
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 809
   states saved        : 668
   state matches       : 225
   transitions         : 1033
   trace steps         : 892
   valid calls         : 434
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp peterson_true.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp peterson_true.c 

=== Stats ===
   time (s)            : 1.53
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 171
   states saved        : 118
   state matches       : 27
   transitions         : 197
   trace steps         : 144
   valid calls         : 219
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp qrcu_false.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 27:
CIVL execution error in p3 (id = 3) (kind: UNDEFINED_VALUE, certainty: PROVEABLE) 
at qrcu_false.c:112.34-46 "readerstart1":
Attempt to read uninitialized variable readerstart1

Call stacks:

process p0 (id=0):
  pthread_join at pthread.cvl:762.2-7 "$wait" called from
  _CIVL_system at qrcu_false.c:135.2-14 "pthread_join"

process p1 (id=1):
  qrcu_reader1 at qrcu_false.c:68.4-9 "myidx"

process p2 (id=2):
  qrcu_reader2 at qrcu_false.c:90.4-9 "myidx"

process p3 (id=3):
  qrcu_updater at qrcu_false.c:112.2-33 "__VERIFIER_atomic_take_snapshot"

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

=== Command ===
civl verify -enablePrintf=false -svcomp qrcu_false.c 

=== Stats ===
   time (s)            : 1.6
   memory (bytes)      : 163053568
   max process count   : 4
   states              : 65
   states saved        : 27
   state matches       : 0
   transitions         : 66
   trace steps         : 26
   valid calls         : 24
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/qrcu_false_log.txt
civl verify -enablePrintf=false -svcomp qrcu_true.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
17s: mem=516Mb trans=80360 traceSteps=51273 explored=68820 saved=39734 prove=326

=== Command ===
civl verify -enablePrintf=false -svcomp qrcu_true.c 

=== Stats ===
   time (s)            : 17.58
   memory (bytes)      : 541065216
   max process count   : 4
   states              : 69002
   states saved        : 39837
   state matches       : 11645
   transitions         : 80646
   trace steps         : 51481
   valid calls         : 98973
   provers             : z3, cvc4, cvc3
   prover calls        : 384

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp read_write_lock_false.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 59:
CIVL execution error 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.c:42.0-3 "int":

Context: true

Assertion: $assert(false)
-> false

Call stacks:

process p0 (id=0):
  pthread_join at pthread.cvl:762.2-7 "$wait" called from
  _CIVL_system at read_write_lock_false.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.c:42.0-3 "int"

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

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

=== Stats ===
   time (s)            : 2.1
   memory (bytes)      : 163053568
   max process count   : 5
   states              : 1758
   states saved        : 1125
   state matches       : 119
   transitions         : 1878
   trace steps         : 1243
   valid calls         : 1615
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/read_write_lock_false_log.txt
civl verify -enablePrintf=false -svcomp read_write_lock_true.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp read_write_lock_true.c 

=== Stats ===
   time (s)            : 2.03
   memory (bytes)      : 163053568
   max process count   : 5
   states              : 1657
   states saved        : 866
   state matches       : 104
   transitions         : 1760
   trace steps         : 969
   valid calls         : 1309
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp szymanski_true.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp szymanski_true.c 

=== Stats ===
   time (s)            : 1.67
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 206
   states saved        : 157
   state matches       : 69
   transitions         : 274
   trace steps         : 225
   valid calls         : 126
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp time_var_mutex_true.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp time_var_mutex_true.c 

=== Stats ===
   time (s)            : 1.78
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 427
   states saved        : 215
   state matches       : 24
   transitions         : 450
   trace steps         : 238
   valid calls         : 924
   provers             : z3, cvc4, cvc3
   prover calls        : 0

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