civl verify -enablePrintf=false -svcomp bigshot_p_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 37:
CIVL execution error in p0 (id = 0) (kind: MEMORY_LEAK, certainty: CONCRETE) 
at Program:0.-1-6 "Program"Program:
The dyscope d0(id=0) has a non-empty heap upon termination.
heap
| objects of malloc 0 at bigshot_p_false-unreach-call.c:13.2-30 "v = malloc(sizeof(char ... )":
| | 0: (CHAR[8])Hop1s0f0o0{[0]='B', [1]='i', [2]='g', [3]='s', [4]='h', [5]='o', [6]='t'}
| objects of malloc 1:
| | 0: (_pthread_gpool_t[])INVALID

Call stacks:

process p0 (id=0):
  terminated

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

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

=== Stats ===
   time (s)            : 1.89
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 71
   states saved        : 38
   state matches       : 0
   transitions         : 71
   trace steps         : 36
   valid calls         : 69
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/bigshot_p_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp bigshot_s2_true-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 37:
CIVL execution error in p0 (id = 0) (kind: MEMORY_LEAK, certainty: CONCRETE) 
at Program:0.-1-6 "Program"Program:
The dyscope d0(id=0) has a non-empty heap upon termination.
heap
| objects of malloc 0 at bigshot_s2_true-unreach-call.c:13.2-30 "v = malloc(sizeof(char ... )":
| | 0: (CHAR[8])Hop1s0f0o0{[0]='B', [1]='i', [2]='g', [3]='s', [4]='h', [5]='o', [6]='t'}
| objects of malloc 1:
| | 0: (_pthread_gpool_t[])INVALID

Call stacks:

process p0 (id=0):
  terminated

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

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

=== Stats ===
   time (s)            : 1.79
   memory (bytes)      : 163053568
   max process count   : 2
   states              : 71
   states saved        : 38
   state matches       : 0
   transitions         : 71
   trace steps         : 36
   valid calls         : 47
   provers             : z3, cvc4, cvc3
   prover calls        : 1

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

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

=== Stats ===
   time (s)            : 1.66
   memory (bytes)      : 163053568
   max process count   : 2
   states              : 73
   states saved        : 40
   state matches       : 0
   transitions         : 72
   trace steps         : 38
   valid calls         : 59
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp -inputNUM=5 fib_bench_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 71:
CIVL execution error in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before fib_bench_false-unreach-call.c:7.12-14.21 "5" from fib_bench_false-unreach-call.c:14.18-21 "NUM":

Context: 0<=-1*X0+9 && 0<=X0+-1

Assertion: $assert(false)
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before fib_bench_false-unreach-call.c:7.12-14.21 "5" from fib_bench_false-unreach-call.c:14.18-21 "NUM"

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

=== Command ===
civl verify -enablePrintf=false -svcomp -inputNUM=5 fib_bench_false-unreach-call.c 

=== Stats ===
   time (s)            : 2.31
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 3477
   states saved        : 2382
   state matches       : 0
   transitions         : 3478
   trace steps         : 2380
   valid calls         : 2559
   provers             : z3, cvc4, cvc3
   prover calls        : 3

=== Result ===
The program MAY NOT be correct.  See CIVLREP/fib_bench_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp -inputNUM=5 fib_bench_longer_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp -inputNUM=5 fib_bench_longer_false-unreach-call.c 

=== Stats ===
   time (s)            : 3.03
   memory (bytes)      : 231211008
   max process count   : 3
   states              : 11161
   states saved        : 7678
   state matches       : 0
   transitions         : 11160
   trace steps         : 7676
   valid calls         : 8335
   provers             : z3, cvc4, cvc3
   prover calls        : 3

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

=== Command ===
civl verify -enablePrintf=false -svcomp -inputNUM=5 fib_bench_longer_true-unreach-call.c 

=== Stats ===
   time (s)            : 2.93
   memory (bytes)      : 231211008
   max process count   : 3
   states              : 11161
   states saved        : 7678
   state matches       : 0
   transitions         : 11160
   trace steps         : 7676
   valid calls         : 8335
   provers             : z3, cvc4, cvc3
   prover calls        : 3

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

=== Command ===
civl verify -enablePrintf=false -svcomp -inputNUM=5 fib_bench_longest_false-unreach-call.c 

=== Stats ===
   time (s)            : 3.04
   memory (bytes)      : 231211008
   max process count   : 3
   states              : 11161
   states saved        : 7678
   state matches       : 0
   transitions         : 11160
   trace steps         : 7676
   valid calls         : 8335
   provers             : z3, cvc4, cvc3
   prover calls        : 3

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

=== Command ===
civl verify -enablePrintf=false -svcomp -inputNUM=5 fib_bench_longest_true-unreach-call.c 

=== Stats ===
   time (s)            : 3.2
   memory (bytes)      : 231211008
   max process count   : 3
   states              : 11161
   states saved        : 7678
   state matches       : 0
   transitions         : 11160
   trace steps         : 7676
   valid calls         : 8335
   provers             : z3, cvc4, cvc3
   prover calls        : 3

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

=== Command ===
civl verify -enablePrintf=false -svcomp -inputNUM=5 fib_bench_true-unreach-call.c 

=== Stats ===
   time (s)            : 3.07
   memory (bytes)      : 231211008
   max process count   : 3
   states              : 11161
   states saved        : 7678
   state matches       : 0
   transitions         : 11160
   trace steps         : 7676
   valid calls         : 8335
   provers             : z3, cvc4, cvc3
   prover calls        : 3

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp -inputSIZE=2 -inputMAX=2 -inputNUM_THREADS=2 indexer_true-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp -inputSIZE=2 -inputMAX=2 -inputNUM_THREADS=2 indexer_true-unreach-call.c 

=== Stats ===
   time (s)            : 2.22
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 2805
   states saved        : 1291
   state matches       : 216
   transitions         : 3020
   trace steps         : 1506
   valid calls         : 5991
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp lazy01_false-unreach-call.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 p3(id=1) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before lazy01_false-unreach-call.c:36.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 lazy01_false-unreach-call.c:48.2-14 "pthread_join"

process p3 (id=1):
  thread3 at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before lazy01_false-unreach-call.c:36.0-3 "int"

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

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

=== Stats ===
   time (s)            : 1.6
   memory (bytes)      : 163053568
   max process count   : 4
   states              : 122
   states saved        : 59
   state matches       : 0
   transitions         : 123
   trace steps         : 58
   valid calls         : 158
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/lazy01_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputEMPTY=-1 -inputFULL=-2 queue_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 144:
CIVL execution error in p2(id=1) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before queue_false-unreach-call.c:7.13-14 "(" from queue_false-unreach-call.c:14.16-20 "SIZE":

Context: 0==(0 == __VERIFIER_nondet_int(1)) ? 1 : 1

Assertion: $assert(false)
-> false

Call stacks:

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

process p2 (id=1):
  t2 at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before queue_false-unreach-call.c:7.13-14 "(" from queue_false-unreach-call.c:14.16-20 "SIZE"

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

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

=== Stats ===
   time (s)            : 2.15
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 672
   states saved        : 367
   state matches       : 14
   transitions         : 687
   trace steps         : 380
   valid calls         : 1653
   provers             : z3, cvc4, cvc3
   prover calls        : 6

=== Result ===
The program MAY NOT be correct.  See CIVLREP/queue_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputEMPTY=-1 -inputFULL=-2 queue_longer_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 144:
CIVL execution error in p2(id=1) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before queue_longer_false-unreach-call.c:6.13-14 "(" from queue_longer_false-unreach-call.c:13.16-20 "SIZE":

Context: 0==(0 == __VERIFIER_nondet_int(1)) ? 1 : 1

Assertion: $assert(false)
-> false

Call stacks:

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

process p2 (id=1):
  t2 at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before queue_longer_false-unreach-call.c:6.13-14 "(" from queue_longer_false-unreach-call.c:13.16-20 "SIZE"

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

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

=== Stats ===
   time (s)            : 2.38
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 672
   states saved        : 367
   state matches       : 14
   transitions         : 687
   trace steps         : 380
   valid calls         : 1653
   provers             : z3, cvc4, cvc3
   prover calls        : 6

=== Result ===
The program MAY NOT be correct.  See CIVLREP/queue_longer_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputEMPTY=-1 -inputFULL=-2 queue_longest_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 144:
CIVL execution error in p2(id=1) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before queue_longest_false-unreach-call.c:6.13-14 "(" from queue_longest_false-unreach-call.c:13.16-20 "SIZE":

Context: 0==(0 == __VERIFIER_nondet_int(1)) ? 1 : 1

Assertion: $assert(false)
-> false

Call stacks:

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

process p2 (id=1):
  t2 at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before queue_longest_false-unreach-call.c:6.13-14 "(" from queue_longest_false-unreach-call.c:13.16-20 "SIZE"

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

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

=== Stats ===
   time (s)            : 2.23
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 672
   states saved        : 367
   state matches       : 14
   transitions         : 687
   trace steps         : 380
   valid calls         : 1653
   provers             : z3, cvc4, cvc3
   prover calls        : 6

=== Result ===
The program MAY NOT be correct.  See CIVLREP/queue_longest_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputEMPTY=-1 -inputFULL=-2 queue_ok_longer_true-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 2.12
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 795
   states saved        : 466
   state matches       : 31
   transitions         : 825
   trace steps         : 496
   valid calls         : 1335
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp -inputSIZE=50 -inputEMPTY=-1 -inputFULL=-2 queue_ok_longest_true-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 2.78
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 4620
   states saved        : 2986
   state matches       : 211
   transitions         : 4830
   trace steps         : 3196
   valid calls         : 8130
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputEMPTY=-1 -inputFULL=-2 queue_ok_true-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 2.15
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 795
   states saved        : 466
   state matches       : 31
   transitions         : 825
   trace steps         : 496
   valid calls         : 1305
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp -inputCIVL_argc=1 reorder_2_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 63:
CIVL execution error in p3(id=3) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before reorder_2_false-unreach-call.c:20.13-17 "argc":

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 reorder_2_false-unreach-call.c:54.24-36 "pthread_join"

process p1 (id=1):
  setThread at reorder_2_false-unreach-call.c:72.4-5 "b"

process p2 (id=2):
  setThread at reorder_2_false-unreach-call.c:72.4-5 "b"

process p3 (id=3):
  checkThread at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before reorder_2_false-unreach-call.c:20.13-17 "argc"

process p4 (id=4):
  checkThread at reorder_2_false-unreach-call.c:78.4-6 "if"

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

=== Command ===
civl verify -enablePrintf=false -svcomp -inputCIVL_argc=1 reorder_2_false-unreach-call.c 

=== Stats ===
   time (s)            : 2.42
   memory (bytes)      : 163053568
   max process count   : 5
   states              : 458
   states saved        : 311
   state matches       : 30
   transitions         : 488
   trace steps         : 340
   valid calls         : 2177
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/reorder_2_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp sigma_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 105:
CIVL execution error in p1 (id = 1) (kind: DEREFERENCE, certainty: PROVEABLE) 
at sigma_false-unreach-call.c:17.1-19 "array[array_index]":
Illegal pointer dereference: Array index out of bounds in method arrayRead.
array: Hop0s0f1o0
extent: 16
index: 16

Call stacks:

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

process p1 (id=1):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p2 (id=2):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p3 (id=3):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p4 (id=4):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p5 (id=5):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p6 (id=6):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p7 (id=7):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p8 (id=8):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p9 (id=9):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p10 (id=10):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p11 (id=11):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p12 (id=12):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p13 (id=13):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p14 (id=14):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p15 (id=15):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

process p16 (id=16):
  thread at sigma_false-unreach-call.c:17.1-19 "array[array_index]"

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

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

=== Stats ===
   time (s)            : 2.19
   memory (bytes)      : 163053568
   max process count   : 17
   states              : 271
   states saved        : 107
   state matches       : 0
   transitions         : 271
   trace steps         : 104
   valid calls         : 141
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The program MAY NOT be correct.  See CIVLREP/sigma_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp singleton_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 80:
CIVL execution error in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-13 "(v[0]) == 'X'\n" inserted by PthreadToCIVLTransformer.assertion before singleton_false-unreach-call.c:47.0-3 "int":

Context: 0<=SIZEOF_CHAR+-1

Assertion: $assert((*((v+0))==X))
-> *(&<d0>heap.malloc0[0][0]+0)=='X'
-> 'Y'=='X'
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at PthreadToCIVLTransformer:0.-1-13 "(v[0]) == 'X'\n" inserted by PthreadToCIVLTransformer.assertion before singleton_false-unreach-call.c:47.0-3 "int"

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

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

=== Stats ===
   time (s)            : 2.11
   memory (bytes)      : 163053568
   max process count   : 6
   states              : 258
   states saved        : 158
   state matches       : 2
   transitions         : 260
   trace steps         : 158
   valid calls         : 213
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/singleton_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp singleton_with-uninit-problems-true.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp singleton_with-uninit-problems-true.c 

=== Stats ===
   time (s)            : 2.13
   memory (bytes)      : 163053568
   max process count   : 6
   states              : 439
   states saved        : 304
   state matches       : 20
   transitions         : 458
   trace steps         : 322
   valid calls         : 436
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 161:
CIVL execution error in p2(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before stack_false-unreach-call.c:9.18-19 "(" from stack_false-unreach-call.c:49.11-19 "OVERFLOW":

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 stack_false-unreach-call.c:116.2-14 "pthread_join"

process p1 (id=1):
  _pthread_mutex_lock at pthread.cvl:832.2-9 "$choose" called from
  t1 at stack_false-unreach-call.c:81.4-22 "pthread_mutex_lock"

process p2 (id=2):
  error at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before stack_false-unreach-call.c:9.18-19 "(" from stack_false-unreach-call.c:49.11-19 "OVERFLOW" called from
  t2 at stack_false-unreach-call.c:100.8-13 "error"

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

=== Command ===
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_false-unreach-call.c 

=== Stats ===
   time (s)            : 2.47
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 1183
   states saved        : 654
   state matches       : 57
   transitions         : 1240
   trace steps         : 710
   valid calls         : 3863
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The program MAY NOT be correct.  See CIVLREP/stack_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longer_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 161:
CIVL execution error in p2(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before stack_longer_false-unreach-call.c:8.18-19 "(" from stack_longer_false-unreach-call.c:46.11-19 "OVERFLOW":

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 stack_longer_false-unreach-call.c:113.2-14 "pthread_join"

process p1 (id=1):
  _pthread_mutex_lock at pthread.cvl:832.2-9 "$choose" called from
  t1 at stack_longer_false-unreach-call.c:78.4-22 "pthread_mutex_lock"

process p2 (id=2):
  error at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before stack_longer_false-unreach-call.c:8.18-19 "(" from stack_longer_false-unreach-call.c:46.11-19 "OVERFLOW" called from
  t2 at stack_longer_false-unreach-call.c:97.8-13 "error"

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

=== Command ===
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longer_false-unreach-call.c 

=== Stats ===
   time (s)            : 2.48
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 1183
   states saved        : 654
   state matches       : 57
   transitions         : 1240
   trace steps         : 710
   valid calls         : 3863
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The program MAY NOT be correct.  See CIVLREP/stack_longer_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longer_true-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longer_true-unreach-call.c 

=== Stats ===
   time (s)            : 4.02
   memory (bytes)      : 231211008
   max process count   : 3
   states              : 12662
   states saved        : 6954
   state matches       : 961
   transitions         : 13622
   trace steps         : 7914
   valid calls         : 51809
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longest_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 161:
CIVL execution error in p2(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before stack_longest_false-unreach-call.c:8.18-19 "(" from stack_longest_false-unreach-call.c:47.11-19 "OVERFLOW":

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 stack_longest_false-unreach-call.c:114.2-14 "pthread_join"

process p1 (id=1):
  _pthread_mutex_lock at pthread.cvl:832.2-9 "$choose" called from
  t1 at stack_longest_false-unreach-call.c:79.4-22 "pthread_mutex_lock"

process p2 (id=2):
  error at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before stack_longest_false-unreach-call.c:8.18-19 "(" from stack_longest_false-unreach-call.c:47.11-19 "OVERFLOW" called from
  t2 at stack_longest_false-unreach-call.c:98.8-13 "error"

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

=== Command ===
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longest_false-unreach-call.c 

=== Stats ===
   time (s)            : 2.53
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 1183
   states saved        : 654
   state matches       : 57
   transitions         : 1240
   trace steps         : 710
   valid calls         : 3863
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The program MAY NOT be correct.  See CIVLREP/stack_longest_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longest_true-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longest_true-unreach-call.c 

=== Stats ===
   time (s)            : 4.25
   memory (bytes)      : 240123904
   max process count   : 3
   states              : 12662
   states saved        : 6954
   state matches       : 961
   transitions         : 13622
   trace steps         : 7914
   valid calls         : 51809
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_true-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_true-unreach-call.c 

=== Stats ===
   time (s)            : 4.04
   memory (bytes)      : 231211008
   max process count   : 3
   states              : 12662
   states saved        : 6954
   state matches       : 961
   transitions         : 13622
   trace steps         : 7914
   valid calls         : 51809
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_true.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -svcomp -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_true.c 

=== Stats ===
   time (s)            : 3.97
   memory (bytes)      : 231211008
   max process count   : 3
   states              : 12662
   states saved        : 6954
   state matches       : 961
   transitions         : 13622
   trace steps         : 7914
   valid calls         : 51809
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp stateful01_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 76:
CIVL execution error in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before stateful01_false-unreach-call.c:32.0-3 "int":

Context: true

Assertion: $assert(false)
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before stateful01_false-unreach-call.c:32.0-3 "int"

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

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

=== Stats ===
   time (s)            : 1.66
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 146
   states saved        : 76
   state matches       : 0
   transitions         : 147
   trace steps         : 75
   valid calls         : 205
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/stateful01_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp stateful01_false.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 76:
CIVL execution error in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before stateful01_false.c:32.0-3 "int":

Context: true

Assertion: $assert(false)
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at PthreadToCIVLTransformer:0.-1-6 "$false\n" inserted by PthreadToCIVLTransformer.assertion before stateful01_false.c:32.0-3 "int"

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

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

=== Stats ===
   time (s)            : 1.74
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 146
   states saved        : 76
   state matches       : 0
   transitions         : 147
   trace steps         : 75
   valid calls         : 205
   provers             : z3, cvc4, cvc3
   prover calls        : 0

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

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

=== Stats ===
   time (s)            : 1.89
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 489
   states saved        : 240
   state matches       : 20
   transitions         : 508
   trace steps         : 259
   valid calls         : 1381
   provers             : z3, cvc4, cvc3
   prover calls        : 0

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

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

=== Stats ===
   time (s)            : 1.81
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 489
   states saved        : 240
   state matches       : 20
   transitions         : 508
   trace steps         : 259
   valid calls         : 1381
   provers             : z3, cvc4, cvc3
   prover calls        : 0

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

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

=== Stats ===
   time (s)            : 2.09
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 332
   states saved        : 186
   state matches       : 10
   transitions         : 341
   trace steps         : 195
   valid calls         : 636
   provers             : z3, cvc4, cvc3
   prover calls        : 0

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

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

=== Stats ===
   time (s)            : 2.17
   memory (bytes)      : 163053568
   max process count   : 3
   states              : 332
   states saved        : 186
   state matches       : 10
   transitions         : 341
   trace steps         : 195
   valid calls         : 636
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -svcomp -inputCIVL_argc=1 twostage_3_false-unreach-call.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 164:
CIVL execution error in p0 (id = 0) (kind: MEMORY_LEAK, certainty: CONCRETE) 
at Program:0.-1-6 "Program"Program:
The dyscope d0(id=0) has a non-empty heap upon termination.
heap
| objects of malloc 0 at twostage_3_false-unreach-call.c:70.4-67 "data1Lock = (pthread_mutex_t *) ... )":
| | 0: (pthread_mutex_t[1]){Hop0s0f0o0[0]{.count=1, .ownerid=$proc_null, .lock=0, .prioceiling={0, 0, 0, 0, 0}}}
| objects of malloc 1 at twostage_3_false-unreach-call.c:71.4-67 "data2Lock = (pthread_mutex_t *) ... )":
| | 0: (pthread_mutex_t[1]){Hop0s0f1o0[0]{.count=1, .ownerid=$proc_null, .lock=0, .prioceiling={0, 0, 0, 0, 0}}}
| objects of malloc 4:
| | 0: (_pthread_gpool_t[])INVALID

Call stacks:

process p0 (id=0):
  terminated

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

=== Command ===
civl verify -enablePrintf=false -svcomp -inputCIVL_argc=1 twostage_3_false-unreach-call.c 

=== Stats ===
   time (s)            : 2.64
   memory (bytes)      : 163053568
   max process count   : 4
   states              : 311
   states saved        : 166
   state matches       : 0
   transitions         : 311
   trace steps         : 163
   valid calls         : 795
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/twostage_3_false-unreach-call_log.txt
civl verify -enablePrintf=false -svcomp -inputCIVL_argc=1 twostage_3_false.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 164:
CIVL execution error in p0 (id = 0) (kind: MEMORY_LEAK, certainty: CONCRETE) 
at Program:0.-1-6 "Program"Program:
The dyscope d0(id=0) has a non-empty heap upon termination.
heap
| objects of malloc 0 at twostage_3_false.c:70.4-67 "data1Lock = (pthread_mutex_t *) ... )":
| | 0: (pthread_mutex_t[1]){Hop0s0f0o0[0]{.count=1, .ownerid=$proc_null, .lock=0, .prioceiling={0, 0, 0, 0, 0}}}
| objects of malloc 1 at twostage_3_false.c:71.4-67 "data2Lock = (pthread_mutex_t *) ... )":
| | 0: (pthread_mutex_t[1]){Hop0s0f1o0[0]{.count=1, .ownerid=$proc_null, .lock=0, .prioceiling={0, 0, 0, 0, 0}}}
| objects of malloc 4:
| | 0: (_pthread_gpool_t[])INVALID

Call stacks:

process p0 (id=0):
  terminated

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

=== Command ===
civl verify -enablePrintf=false -svcomp -inputCIVL_argc=1 twostage_3_false.c 

=== Stats ===
   time (s)            : 2.56
   memory (bytes)      : 163053568
   max process count   : 4
   states              : 311
   states saved        : 166
   state matches       : 0
   transitions         : 311
   trace steps         : 163
   valid calls         : 795
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/twostage_3_false_log.txt
