civl verify -enablePrintf=false -inputB=5 adder.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -inputB=5 adder.cvl 

=== Stats ===
   time (s)            : 1.36
   memory (bytes)      : 128974848
   max process count   : 6
   states              : 785
   states saved        : 627
   state matches       : 72
   transitions         : 856
   trace steps         : 688
   valid calls         : 5120
   provers             : z3, cvc4, cvc3
   prover calls        : 21

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -inputB=4 -min adderBad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 27:
CIVL execution error in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at adderBad.cvl:45.2-23 "$assert((seq == par))":

Context: true

Assertion: $assert((seq==par))
-> X1[1]+X1[0]==X1[1]
-> 0==X1[0]

Call stacks:

process p0 (id=0):
  _CIVL_system at adderBad.cvl:45.2-9 "$assert"

Logging new entry 0, writing trace to CIVLREP/adderBad_0.trace
Restricting search depth to 26

=== Command ===
civl verify -enablePrintf=false -inputB=4 -min adderBad.cvl 

=== Stats ===
   time (s)            : 1.16
   memory (bytes)      : 128974848
   max process count   : 5
   states              : 211
   states saved        : 146
   state matches       : 5
   transitions         : 215
   trace steps         : 142
   valid calls         : 319
   provers             : z3, cvc4, cvc3
   prover calls        : 19

=== Result ===
The program MAY NOT be correct.  See CIVLREP/adderBad_log.txt
civl replay adderBad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0:
CIVL execution error in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at adderBad.cvl:45.2-23 "$assert((seq == par))":

Context: true

Assertion: $assert((seq==par))
-> X1[1]+X1[0]==X1[1]
-> 0==X1[0]
State -1:138
| Path condition
| | true
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | B = 4
| | | | N = 2
| | | | a = (real[2])X1
| | dyscope d1 (id=1, parent=d0, static=6)
| | | variables
| | | | seq = X1[1]+X1[0]
| | | | par = X1[1]
| | dyscope d2 (id=2, parent=d0, static=4)
| | | variables
| | | | p = &<d0>a[0]
| | | | n = 2
| | dyscope d3 (id=3, parent=d2, static=7)
| | | variables
| | | | s = X1[1]+X1[0]
| | dyscope d4 (id=4, parent=d3, static=8)
| | | variables
| | | | i = 2
| | dyscope d5 (id=5, parent=d0, static=5)
| | | variables
| | | | p = &<d0>a[0]
| | | | n = 2
| | dyscope d6 (id=6, parent=d5, static=9)
| | | variables
| | | | s = X1[1]
| | | | workers = (process[2]){UNDEFINED, UNDEFINED}
| | dyscope d7 (id=7, parent=d6, static=11)
| | | variables
| | | | j = 2
| | dyscope d8 (id=8, parent=d6, static=10)
| | | variables
| | | | i = 0
| | dyscope d9 (id=9, parent=d8, static=13)
| | | variables
| | | | t = X1[0]
| | dyscope d10 (id=10, parent=d6, static=10)
| | | variables
| | | | i = 1
| | dyscope d11 (id=11, parent=d10, static=13)
| | | variables
| | | | t = X1[1]
| | dyscope d12 (id=12, parent=d6, static=12)
| | | variables
| | | | j = 2
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=6, adderBad.cvl:45.2-9 "$assert", dyscope=d1]
| | process - (id=1): null
| | process - (id=2): null

Trace ends after 27 transitions.
Violation(s) found.

=== Command ===
civl replay adderBad.cvl 

=== Stats ===
   time (s)            : 1.16
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 46
   states Saved        : 32
   valid calls         : 72
   provers             : z3, cvc4, cvc3
   prover calls        : 15

civl verify -enablePrintf=false -inputNUM_ACCOUNTS=3 bank.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -inputNUM_ACCOUNTS=3 bank.cvl 

=== Stats ===
   time (s)            : 1.25
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 1139
   states saved        : 605
   state matches       : 82
   transitions         : 1220
   trace steps         : 686
   valid calls         : 759
   provers             : z3, cvc4, cvc3
   prover calls        : 0

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

=== Command ===
civl verify -enablePrintf=false -inputB=6 barrier.cvl 

=== Stats ===
   time (s)            : 6.41
   memory (bytes)      : 647495680
   max process count   : 7
   states              : 216721
   states saved        : 61044
   state matches       : 71034
   transitions         : 287754
   trace steps         : 132067
   valid calls         : 279236
   provers             : z3, cvc4, cvc3
   prover calls        : 21

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

=== Command ===
civl verify -enablePrintf=false -inputB=4 barrier2.cvl 

=== Stats ===
   time (s)            : 1.78
   memory (bytes)      : 163053568
   max process count   : 5
   states              : 4760
   states saved        : 1939
   state matches       : 676
   transitions         : 5435
   trace steps         : 2608
   valid calls         : 22050
   provers             : z3, cvc4, cvc3
   prover calls        : 17

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -inputB=4 -min barrierBad.cvl 
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 41:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at barrierBad.cvl:44.26-31 "$wait":
A deadlock is possible:
  Path condition: true
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p3 (id=2): false

Call stacks:

process p0 (id=0):
  _CIVL_system at barrierBad.cvl:44.26-31 "$wait"

process p1 (id=1):
  barrier at barrierBad.cvl:25.30-31 ";" called from
  run at barrierBad.cvl:33.4-11 "barrier"

process p3 (id=2):
  barrier at barrierBad.cvl:25.30-31 ";" called from
  run at barrierBad.cvl:33.4-11 "barrier"

Logging new entry 0, writing trace to CIVLREP/barrierBad_0.trace
Restricting search depth to 40

=== Command ===
civl verify -enablePrintf=false -inputB=4 -min barrierBad.cvl 

=== Stats ===
   time (s)            : 1.4
   memory (bytes)      : 128974848
   max process count   : 5
   states              : 2361
   states saved        : 1385
   state matches       : 1655
   transitions         : 4015
   trace steps         : 3033
   valid calls         : 6125
   provers             : z3, cvc4, cvc3
   prover calls        : 13

=== Result ===
The program MAY NOT be correct.  See CIVLREP/barrierBad_log.txt
civl replay -id=0 barrierBad.cvl 
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

State 42
| Path condition
| | true
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | B = 4
| | | | N = 2
| | | | threads = (process[2]){p1, p2}
| | | | in_barrier = (int[2]){1, 1}
| | | | num_in_barrier = 1
| | | | counter = 2
| | dyscope d1 (id=1, parent=d0, static=4)
| | | variables
| | dyscope d2 (id=2, parent=d1, static=9)
| | | variables
| | | | i = 2
| | dyscope d3 (id=3, parent=d0, static=7)
| | | variables
| | | | i = 2
| | dyscope d4 (id=4, parent=d0, static=6)
| | | variables
| | | | tid = 0
| | dyscope d5 (id=5, parent=d0, static=6)
| | | variables
| | | | tid = 1
| | dyscope d6 (id=6, parent=d0, static=8)
| | | variables
| | | | i = 0
| | dyscope d7 (id=7, parent=d0, static=5)
| | | variables
| | | | tid = 0
| | dyscope d8 (id=8, parent=d0, static=5)
| | | variables
| | | | tid = 1
| | dyscope d9 (id=9, parent=d8, static=10)
| | | variables
| | | | i = 2
| | dyscope d7 (id=10, parent=d0, static=5)
| | | variables
| | | | tid = 0
| | dyscope d8 (id=11, parent=d0, static=5)
| | | variables
| | | | tid = 1
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=13, barrierBad.cvl:44.26-31 "$wait", dyscope=d6]
| | process p1(id=1)
| | | call stack
| | | | Frame[function=barrier, location=30, barrierBad.cvl:25.30-31 ";", dyscope=d7]
| | | | Frame[function=run, location=37, barrierBad.cvl:33.4-11 "barrier", dyscope=d4]
| | process p2(id=2)
| | | call stack
| | | | Frame[function=barrier, location=30, barrierBad.cvl:25.30-31 ";", dyscope=d8]
| | | | Frame[function=run, location=37, barrierBad.cvl:33.4-11 "barrier", dyscope=d5]

Violation of Deadlock found in State 42:
A deadlock is possible:
  Path condition: true
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): false

Trace ends after 40 transitions.
Violation(s) found.

=== Command ===
civl replay -id=0 barrierBad.cvl 

=== Stats ===
   time (s)            : 0.92
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 63
   states Saved        : 43
   valid calls         : 152
   provers             : z3, cvc4, cvc3
   prover calls        : 9

civl verify -enablePrintf=false -inputB=6 -inputW=3 blockAdder.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -inputB=6 -inputW=3 blockAdder.cvl 

=== Stats ===
   time (s)            : 1.62
   memory (bytes)      : 128974848
   max process count   : 4
   states              : 1178
   states saved        : 690
   state matches       : 36
   transitions         : 1213
   trace steps         : 691
   valid calls         : 3066
   provers             : z3, cvc4, cvc3
   prover calls        : 31

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -inputB=6 -inputW=3 -min blockAdderBad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 29:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at blockAdderBad.cvl:46.2-10 "$waitall":
A deadlock is possible:
  Path condition: true
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): terminated
process p3 (id=2): false

Call stacks:

process p0 (id=0):
  adder_par at blockAdderBad.cvl:46.2-10 "$waitall" called from
  _CIVL_system at blockAdderBad.cvl:52.19-28 "adder_par"

process p1 (id=1):
  terminated

process p3 (id=2):
  run_worker at blockAdderBad.cvl:38.20-24 "lock"

Logging new entry 0, writing trace to CIVLREP/blockAdderBad_0.trace
Restricting search depth to 28

=== Command ===
civl verify -enablePrintf=false -inputB=6 -inputW=3 -min blockAdderBad.cvl 

=== Stats ===
   time (s)            : 1.44
   memory (bytes)      : 128974848
   max process count   : 4
   states              : 385
   states saved        : 277
   state matches       : 0
   transitions         : 384
   trace steps         : 242
   valid calls         : 636
   provers             : z3, cvc4, cvc3
   prover calls        : 31

=== Result ===
The program MAY NOT be correct.  See CIVLREP/blockAdderBad_log.txt
civl replay blockAdderBad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

State 31
| Path condition
| | true
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | B = 6
| | | | W = 3
| | | | N = 1
| | | | P = 2
| | | | a = (real[1])X2
| | dyscope d1 (id=1, parent=d0, static=6)
| | | variables
| | | | sum_seq = X2[0]
| | | | sum_par = NULL
| | dyscope d2 (id=2, parent=d0, static=4)
| | | variables
| | dyscope d3 (id=3, parent=d2, static=7)
| | | variables
| | | | s = X2[0]
| | dyscope d4 (id=4, parent=d3, static=8)
| | | variables
| | | | i = 1
| | dyscope d5 (id=5, parent=d0, static=5)
| | | variables
| | dyscope d6 (id=6, parent=d5, static=9)
| | | variables
| | | | workers = (process[2]){p1, p2}
| | | | lock = 1
| | | | result = 0
| | dyscope d7 (id=7, parent=d6, static=11)
| | | variables
| | | | i = 2
| | dyscope d8 (id=8, parent=d6, static=12)
| | | variables
| | | | i = 2
| | dyscope d9 (id=9, parent=d6, static=10)
| | | variables
| | | | id = 0
| | dyscope d10 (id=10, parent=d9, static=13)
| | | variables
| | | | start = 0
| | | | stop = 0
| | | | localSum = 0
| | dyscope d11 (id=11, parent=d6, static=10)
| | | variables
| | | | id = 1
| | dyscope d12 (id=12, parent=d11, static=13)
| | | variables
| | | | start = 0
| | | | stop = 1
| | | | localSum = X2[0]
| | dyscope d13 (id=13, parent=d10, static=14)
| | | variables
| | | | i = 0
| | dyscope d14 (id=14, parent=d12, static=14)
| | | variables
| | | | i = 1
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=adder_par, location=24, blockAdderBad.cvl:46.2-10 "$waitall", dyscope=d6]
| | | | Frame[function=_CIVL_system, location=8, blockAdderBad.cvl:52.19-28 "adder_par", dyscope=d1]
| | process p1(id=1)
| | | call stack
| | process p2(id=2)
| | | call stack
| | | | Frame[function=run_worker, location=34, blockAdderBad.cvl:38.20-24 "lock", dyscope=d12]

Violation of Deadlock found in State 31:
A deadlock is possible:
  Path condition: true
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): terminated
process p2 (id=2): false

Trace ends after 28 transitions.
Violation(s) found.

=== Command ===
civl replay blockAdderBad.cvl 

=== Stats ===
   time (s)            : 1.01
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 50
   states Saved        : 32
   valid calls         : 136
   provers             : z3, cvc4, cvc3
   prover calls        : 15

civl verify -enablePrintf=false boundedBuffer.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 37:
CIVL execution error in p2(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at boundedBuffer.cvl:37.4-26 "$assert(fillCount > 0)":

Context: true

Assertion: $assert((0<fillCount))
-> 0<0
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at boundedBuffer.cvl:53.2-10 "$waitall"

process p1 (id=1):
  consumer at boundedBuffer.cvl:36.24-25 ";"

process p2 (id=2):
  consumer at boundedBuffer.cvl:37.4-11 "$assert"

process p3 (id=3):
  producer at boundedBuffer.cvl:26.25-26 ";"

process p4 (id=4):
  producer at boundedBuffer.cvl:26.25-26 ";"

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

=== Command ===
civl verify -enablePrintf=false boundedBuffer.cvl 

=== Stats ===
   time (s)            : 1.23
   memory (bytes)      : 128974848
   max process count   : 5
   states              : 54
   states saved        : 42
   state matches       : 5
   transitions         : 59
   trace steps         : 46
   valid calls         : 174
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/boundedBuffer_log.txt
civl verify -enablePrintf=false -min boundedBuffer_bad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 55:
CIVL execution error in p2(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at boundedBuffer_bad.cvl:40.4-26 "$assert(fillCount > 0)":

Context: true

Assertion: $assert((0<fillCount))
-> 0<0
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at boundedBuffer_bad.cvl:56.2-10 "$waitall"

process p1 (id=1):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p2 (id=2):
  consumer at boundedBuffer_bad.cvl:40.4-11 "$assert"

process p3 (id=3):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p4 (id=4):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p5 (id=5):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p6 (id=6):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p7 (id=7):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p8 (id=8):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p9 (id=9):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p10 (id=10):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

Logging new entry 0, writing trace to CIVLREP/boundedBuffer_bad_0.trace
Restricting search depth to 54
Error 1 encountered at depth 53:
CIVL execution error in p2(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at boundedBuffer_bad.cvl:40.4-26 "$assert(fillCount > 0)":

Context: true

Assertion: $assert((0<fillCount))
-> 0<0
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at boundedBuffer_bad.cvl:56.2-10 "$waitall"

process p1 (id=1):
  consumer at boundedBuffer_bad.cvl:43.4-14 "emptyCount"

process p2 (id=2):
  consumer at boundedBuffer_bad.cvl:40.4-11 "$assert"

process p3 (id=3):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p4 (id=4):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p5 (id=5):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p6 (id=6):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p7 (id=7):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p8 (id=8):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p9 (id=9):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p10 (id=10):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

New log entry is equivalent to previously encountered entry 0
Length of new trace (53) is less than length of old (55): replacing old with new...
Restricting search depth to 52
Error 2 encountered at depth 51:
CIVL execution error in p3(id=3) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at boundedBuffer_bad.cvl:40.4-26 "$assert(fillCount > 0)":

Context: true

Assertion: $assert((0<fillCount))
-> 0<0
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at boundedBuffer_bad.cvl:56.2-10 "$waitall"

process p1 (id=1):
  consumer at boundedBuffer_bad.cvl:43.4-14 "emptyCount"

process p2 (id=2):
  consumer at boundedBuffer_bad.cvl:43.4-14 "emptyCount"

process p3 (id=3):
  consumer at boundedBuffer_bad.cvl:40.4-11 "$assert"

process p4 (id=4):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p5 (id=5):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p6 (id=6):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p7 (id=7):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p8 (id=8):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p9 (id=9):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p10 (id=10):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

New log entry is equivalent to previously encountered entry 0
Length of new trace (51) is less than length of old (53): replacing old with new...
Restricting search depth to 50
Error 3 encountered at depth 45:
CIVL execution error in p2(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at boundedBuffer_bad.cvl:40.4-26 "$assert(fillCount > 0)":

Context: true

Assertion: $assert((0<fillCount))
-> 0<0
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at boundedBuffer_bad.cvl:56.2-10 "$waitall"

process p1 (id=1):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p2 (id=2):
  consumer at boundedBuffer_bad.cvl:40.4-11 "$assert"

process p3 (id=3):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p4 (id=4):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p5 (id=5):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p6 (id=6):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p7 (id=7):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p8 (id=8):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p9 (id=9):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p10 (id=10):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

New log entry is equivalent to previously encountered entry 0
Length of new trace (45) is less than length of old (51): replacing old with new...
Restricting search depth to 44
Error 4 encountered at depth 43:
CIVL execution error in p2(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at boundedBuffer_bad.cvl:40.4-26 "$assert(fillCount > 0)":

Context: true

Assertion: $assert((0<fillCount))
-> 0<0
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at boundedBuffer_bad.cvl:56.2-10 "$waitall"

process p1 (id=1):
  consumer at boundedBuffer_bad.cvl:43.4-14 "emptyCount"

process p2 (id=2):
  consumer at boundedBuffer_bad.cvl:40.4-11 "$assert"

process p3 (id=3):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p4 (id=4):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p5 (id=5):
  consumer at boundedBuffer_bad.cvl:39.24-25 ";"

process p6 (id=6):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p7 (id=7):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p8 (id=8):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p9 (id=9):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

process p10 (id=10):
  producer at boundedBuffer_bad.cvl:29.25-26 ";"

New log entry is equivalent to previously encountered entry 0
Length of new trace (43) is less than length of old (45): replacing old with new...
Restricting search depth to 42

=== Command ===
civl verify -enablePrintf=false -min boundedBuffer_bad.cvl 

=== Stats ===
   time (s)            : 2.56
   memory (bytes)      : 238026752
   max process count   : 11
   states              : 3156
   states saved        : 3138
   state matches       : 5231
   transitions         : 8895
   trace steps         : 8877
   valid calls         : 60905
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/boundedBuffer_bad_log.txt
civl replay boundedBuffer_bad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0:
CIVL execution error in p2(id=2) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at boundedBuffer_bad.cvl:40.4-26 "$assert(fillCount > 0)":

Context: true

Assertion: $assert((0<fillCount))
-> 0<0
-> false
State -1:187
| Path condition
| | true
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | BUFFER_SIZE = 100
| | | | NPRODUCER = 5
| | | | NCONSUMER = 5
| | | | fillCount = 0
| | | | emptyCount = 99
| | dyscope d1 (id=1, parent=d0, static=5)
| | | variables
| | | | producers = (process[5]){p6, p7, p8, p9, p10}
| | | | consumers = (process[5]){p1, p2, p3, p4, p5}
| | dyscope d2 (id=2, parent=d1, static=6)
| | | variables
| | | | i = 5
| | dyscope d3 (id=3, parent=d0, static=4)
| | | variables
| | dyscope d4 (id=4, parent=d0, static=4)
| | | variables
| | dyscope d5 (id=5, parent=d0, static=4)
| | | variables
| | dyscope d6 (id=6, parent=d0, static=4)
| | | variables
| | dyscope d7 (id=7, parent=d0, static=4)
| | | variables
| | dyscope d8 (id=8, parent=d1, static=7)
| | | variables
| | | | i = 5
| | dyscope d9 (id=9, parent=d0, static=3)
| | | variables
| | dyscope d10 (id=10, parent=d0, static=3)
| | | variables
| | dyscope d11 (id=11, parent=d0, static=3)
| | | variables
| | dyscope d12 (id=12, parent=d0, static=3)
| | | variables
| | dyscope d13 (id=13, parent=d0, static=3)
| | | variables
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=11, boundedBuffer_bad.cvl:56.2-10 "$waitall", dyscope=d1]
| | process p1(id=1)
| | | call stack
| | | | Frame[function=consumer, location=29, boundedBuffer_bad.cvl:43.4-14 "emptyCount", dyscope=d3]
| | process p2(id=2)
| | | call stack
| | | | Frame[function=consumer, location=27, boundedBuffer_bad.cvl:40.4-11 "$assert", dyscope=d4]
| | process p3(id=3)
| | | call stack
| | | | Frame[function=consumer, location=26, boundedBuffer_bad.cvl:39.24-25 ";", dyscope=d5]
| | process p4(id=4)
| | | call stack
| | | | Frame[function=consumer, location=26, boundedBuffer_bad.cvl:39.24-25 ";", dyscope=d6]
| | process p5(id=5)
| | | call stack
| | | | Frame[function=consumer, location=26, boundedBuffer_bad.cvl:39.24-25 ";", dyscope=d7]
| | process p6(id=6)
| | | call stack
| | | | Frame[function=producer, location=20, boundedBuffer_bad.cvl:29.25-26 ";", dyscope=d9]
| | process p7(id=7)
| | | call stack
| | | | Frame[function=producer, location=20, boundedBuffer_bad.cvl:29.25-26 ";", dyscope=d10]
| | process p8(id=8)
| | | call stack
| | | | Frame[function=producer, location=20, boundedBuffer_bad.cvl:29.25-26 ";", dyscope=d11]
| | process p9(id=9)
| | | call stack
| | | | Frame[function=producer, location=20, boundedBuffer_bad.cvl:29.25-26 ";", dyscope=d12]
| | process p10(id=10)
| | | call stack
| | | | Frame[function=producer, location=20, boundedBuffer_bad.cvl:29.25-26 ";", dyscope=d13]

Trace ends after 43 transitions.
Violation(s) found.

=== Command ===
civl replay boundedBuffer_bad.cvl 

=== Stats ===
   time (s)            : 0.82
   memory (bytes)      : 128974848
   max process count   : 11
   states              : 61
   states Saved        : 43
   valid calls         : 285
   provers             : z3, cvc4, cvc3
   prover calls        : 0

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

=== Command ===
civl verify -enablePrintf=false dining.cvl 

=== Stats ===
   time (s)            : 1.1
   memory (bytes)      : 128974848
   max process count   : 5
   states              : 435
   states saved        : 294
   state matches       : 167
   transitions         : 601
   trace steps         : 456
   valid calls         : 1861
   provers             : z3, cvc4, cvc3
   prover calls        : 9

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -min diningBad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 5:
CIVL execution error in p0(id=0) (kind: OTHER, certainty: PROVEABLE) 
at diningBad.cvl:32.2-9 "$parfor":
The arguments of the domain for $parfor must be concrete.

Call stacks:

process p0 (id=0):
  _CIVL_system at diningBad.cvl:32.2-9 "$parfor"

Logging new entry 0, writing trace to CIVLREP/diningBad_0.trace
Restricting search depth to 4
Error 1 encountered at depth 5:
CIVL execution error in p0(id=0) (kind: OTHER, certainty: PROVEABLE) 
at diningBad.cvl:32.2-32 "$parfor (int i :  ... ;":
The number of processes for $waitall needs a concrete value.

Call stacks:

process p0 (id=0):
  _CIVL_system at diningBad.cvl:32.31-32 ";"

Logging new entry 1, writing trace to CIVLREP/diningBad_1.trace
Restricting search depth to 4
Error 2 encountered at depth 5:
CIVL execution error in p0(id=0) (kind: OTHER, certainty: PROVEABLE) 
at diningBad.cvl:32.2-32 "$parfor (int i :  ... ;":
The number of processes for $waitall needs a concrete value.

Call stacks:

process p0 (id=0):
  _CIVL_system at diningBad.cvl:32.31-32 ";"

New log entry is equivalent to previously encountered entry 1
Length of new trace (5) is greater than or equal to length of old (5): ignoring new trace.
Restricting search depth to 4
Error 3 encountered at depth 6:
CIVL execution error in p0(id=0) (kind: OTHER, certainty: PROVEABLE) 
at diningBad.cvl:32.2-32 "$parfor (int i :  ... ;":
The number of processes for $waitall needs a concrete value.

Call stacks:

process p0 (id=0):
  _CIVL_system at diningBad.cvl:32.31-32 ";"

New log entry is equivalent to previously encountered entry 1
Length of new trace (6) is greater than or equal to length of old (5): ignoring new trace.
Restricting search depth to 5
Error 4 encountered at depth 6:
CIVL execution error in p0(id=0) (kind: OTHER, certainty: PROVEABLE) 
at diningBad.cvl:32.2-32 "$parfor (int i :  ... ;":
The number of processes for $waitall needs a concrete value.

Call stacks:

process p0 (id=0):
  _CIVL_system at diningBad.cvl:32.31-32 ";"

New log entry is equivalent to previously encountered entry 1
Length of new trace (6) is greater than or equal to length of old (5): ignoring new trace.
Restricting search depth to 5
Error 5 encountered at depth 6:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at diningBad.cvl:32.31-32 ";":
A deadlock is possible:
  Path condition: (0 <= -1*X0+7) && (0 <= X0+-2)
  Enabling predicate: false
process p0 (id=0): false

Call stacks:

process p0 (id=0):
  _CIVL_system at diningBad.cvl:32.31-32 ";"

Logging new entry 2, writing trace to CIVLREP/diningBad_2.trace
Restricting search depth to 5

=== Command ===
civl verify -enablePrintf=false -min diningBad.cvl 

=== Stats ===
   time (s)            : 0.82
   memory (bytes)      : 128974848
   max process count   : 1
   states              : 12
   states saved        : 6
   state matches       : 0
   transitions         : 11
   trace steps         : 5
   valid calls         : 18
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The program MAY NOT be correct.  See CIVLREP/diningBad_log.txt
civl replay diningBad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0:
CIVL execution error in p0(id=0) (kind: OTHER, certainty: PROVEABLE) 
at diningBad.cvl:32.2-9 "$parfor":
The arguments of the domain for $parfor must be concrete.
State -1:39
| Path condition
| | (0 <= -1*X0+7) && (0 <= X0+-2)
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | B = 7
| | | | n = X0
| | | | forks = (int[X0])(lambda i : int . 0){[0]=0}
| | dyscope d1 (id=1, parent=d0, static=4)
| | | variables
| | | | philosophers = (process[X0])X_s1v1p0
| | | | dom = ($domain){1, 0, inject(0,($regular_range[1])<$regular_range<0,X0+-1,1>>)}
| | | | _dom_size0 = X0
| | | | _par_procs0 = NULL
| | dyscope d2 (id=2, parent=d1, static=5)
| | | variables
| | | | i = 0
| | | | __LiteralDomain_counter0__ = NULL
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=7, diningBad.cvl:32.2-9 "$parfor", dyscope=d1]

Error 1:
CIVL execution error in p0(id=0) (kind: OTHER, certainty: PROVEABLE) 
at diningBad.cvl:32.2-32 "$parfor (int i :  ... ;":
The number of processes for $waitall needs a concrete value.
State -1:40
| Path condition
| | (0 <= -1*X0+7) && (0 <= X0+-2)
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | B = 7
| | | | n = X0
| | | | forks = (int[X0])(lambda i : int . 0){[0]=0}
| | dyscope d1 (id=1, parent=d0, static=4)
| | | variables
| | | | philosophers = (process[X0])X_s1v1p0
| | | | dom = ($domain){1, 0, inject(0,($regular_range[1])<$regular_range<0,X0+-1,1>>)}
| | | | _dom_size0 = X0
| | | | _par_procs0 = NULL
| | dyscope d2 (id=2, parent=d1, static=5)
| | | variables
| | | | i = 0
| | | | __LiteralDomain_counter0__ = NULL
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=8, diningBad.cvl:32.31-32 ";", dyscope=d1]

Error 2:
CIVL execution error in p0(id=0) (kind: OTHER, certainty: PROVEABLE) 
at diningBad.cvl:32.2-32 "$parfor (int i :  ... ;":
The number of processes for $waitall needs a concrete value.
State 5
| Path condition
| | (0 <= -1*X0+7) && (0 <= X0+-2)
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | B = 7
| | | | n = X0
| | | | forks = (int[X0])(lambda i : int . 0){[0]=0}
| | dyscope d1 (id=1, parent=d0, static=4)
| | | variables
| | | | philosophers = (process[X0])X_s1v1p0
| | | | dom = ($domain){1, 0, inject(0,($regular_range[1])<$regular_range<0,X0+-1,1>>)}
| | | | _dom_size0 = X0
| | | | _par_procs0 = NULL
| | dyscope d2 (id=2, parent=d1, static=5)
| | | variables
| | | | i = 0
| | | | __LiteralDomain_counter0__ = NULL
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=8, diningBad.cvl:32.31-32 ";", dyscope=d1]

Error 3:
CIVL execution error in p0(id=0) (kind: OTHER, certainty: PROVEABLE) 
at diningBad.cvl:32.2-32 "$parfor (int i :  ... ;":
The number of processes for $waitall needs a concrete value.
State 5
| Path condition
| | (0 <= -1*X0+7) && (0 <= X0+-2)
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | B = 7
| | | | n = X0
| | | | forks = (int[X0])(lambda i : int . 0){[0]=0}
| | dyscope d1 (id=1, parent=d0, static=4)
| | | variables
| | | | philosophers = (process[X0])X_s1v1p0
| | | | dom = ($domain){1, 0, inject(0,($regular_range[1])<$regular_range<0,X0+-1,1>>)}
| | | | _dom_size0 = X0
| | | | _par_procs0 = NULL
| | dyscope d2 (id=2, parent=d1, static=5)
| | | variables
| | | | i = 0
| | | | __LiteralDomain_counter0__ = NULL
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=8, diningBad.cvl:32.31-32 ";", dyscope=d1]


State 5
| Path condition
| | (0 <= -1*X0+7) && (0 <= X0+-2)
| Dynamic scopes
| | dyscope d0 (id=0, parent=NULL, static=0)
| | | variables
| | | | B = 7
| | | | n = X0
| | | | forks = (int[X0])(lambda i : int . 0){[0]=0}
| | dyscope d1 (id=1, parent=d0, static=4)
| | | variables
| | | | philosophers = (process[X0])X_s1v1p0
| | | | dom = ($domain){1, 0, inject(0,($regular_range[1])<$regular_range<0,X0+-1,1>>)}
| | | | _dom_size0 = X0
| | | | _par_procs0 = NULL
| | dyscope d2 (id=2, parent=d1, static=5)
| | | variables
| | | | i = 0
| | | | __LiteralDomain_counter0__ = NULL
| Process states
| | process p0(id=0)
| | | call stack
| | | | Frame[function=_CIVL_system, location=8, diningBad.cvl:32.31-32 ";", dyscope=d1]

Violation of Deadlock found in State 5:
A deadlock is possible:
  Path condition: (0 <= -1*X0+7) && (0 <= X0+-2)
  Enabling predicate: false
process p0 (id=0): false

Trace ends after 5 transitions.
Violation(s) found.

=== Command ===
civl replay diningBad.cvl 

=== Stats ===
   time (s)            : 0.78
   memory (bytes)      : 128974848
   max process count   : 1
   states              : 12
   states Saved        : 6
   valid calls         : 18
   provers             : z3, cvc4, cvc3
   prover calls        : 2

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

=== Command ===
civl verify -enablePrintf=false dlqueue.cvl 

=== Stats ===
   time (s)            : 1.06
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 109
   states saved        : 93
   state matches       : 1
   transitions         : 109
   trace steps         : 88
   valid calls         : 52
   provers             : z3, cvc4, cvc3
   prover calls        : 1

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

=== Command ===
civl verify -enablePrintf=false exitBarrier.cvl 

=== Stats ===
   time (s)            : 1.6
   memory (bytes)      : 128974848
   max process count   : 5
   states              : 1268
   states saved        : 1074
   state matches       : 168
   transitions         : 1435
   trace steps         : 1241
   valid calls         : 4681
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -inputNPROCS=2 hybrid.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 254:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at mp_root2.cvh:67.4-9 "$wait" included from hybrid.cvl:6.9-23 ""mp_root2.cvh"":
A deadlock is possible:
  Path condition: 0 <= SIZEOF_INT+-1
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): false
process p3 (id=3): false
process p4 (id=4): false
process p5 (id=5): false

Call stacks:

process p0 (id=0):
  finalize at mp_root2.cvh:67.4-9 "$wait" included from hybrid.cvl:6.9-23 ""mp_root2.cvh"" called from
  _CIVL_system at mp_root2.cvh:73.2-10 "finalize" included from hybrid.cvl:6.9-23 ""mp_root2.cvh""

process p1 (id=1):
  MPI_Process at hybrid.cvl:39.26-31 "$wait"

process p2 (id=2):
  MPI_Process at hybrid.cvl:39.26-31 "$wait"

process p3 (id=3):
  MPI_Recv at mp_proc2.cvh:45.16-29 "$comm_dequeue" included from hybrid.cvl:10.9-23 ""mp_proc2.cvh"" called from
  Thread at hybrid.cvl:29.10-18 "MPI_Recv"

process p4 (id=4):
  MPI_Recv at mp_proc2.cvh:45.16-29 "$comm_dequeue" included from hybrid.cvl:10.9-23 ""mp_proc2.cvh"" called from
  Thread at hybrid.cvl:29.10-18 "MPI_Recv"

process p5 (id=5):
  MPI_Recv at mp_proc2.cvh:45.16-29 "$comm_dequeue" included from hybrid.cvl:10.9-23 ""mp_proc2.cvh"" called from
  Thread at hybrid.cvl:26.10-18 "MPI_Recv"

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

=== Command ===
civl verify -enablePrintf=false -inputNPROCS=2 hybrid.cvl 

=== Stats ===
   time (s)            : 3.5
   memory (bytes)      : 239599616
   max process count   : 7
   states              : 6779
   states saved        : 4368
   state matches       : 145
   transitions         : 6923
   trace steps         : 4094
   valid calls         : 36392
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/hybrid_log.txt
civl verify -enablePrintf=false locksBad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 6:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at locksBad.cvl:31.2-7 "$wait":
A deadlock is possible:
  Path condition: true
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): false

Call stacks:

process p0 (id=0):
  _CIVL_system at locksBad.cvl:31.2-7 "$wait"

process p1 (id=1):
  proc0 at locksBad.cvl:12.19-24 "lock1"

process p2 (id=2):
  proc1 at locksBad.cvl:21.19-24 "lock0"

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

=== Command ===
civl verify -enablePrintf=false locksBad.cvl 

=== Stats ===
   time (s)            : 0.73
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 12
   states saved        : 9
   state matches       : 1
   transitions         : 12
   trace steps         : 9
   valid calls         : 1
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/locksBad_log.txt
civl verify -enablePrintf=false locksBad10.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 55:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at locksBad10.cvl:32.2-7 "$wait":
A deadlock is possible:
  Path condition: true
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): false

Call stacks:

process p0 (id=0):
  _CIVL_system at locksBad10.cvl:32.2-7 "$wait"

process p1 (id=1):
  f at locksBad10.cvl:12.17-18 "y"

process p2 (id=2):
  g at locksBad10.cvl:21.17-18 "x"

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

=== Command ===
civl verify -enablePrintf=false locksBad10.cvl 

=== Stats ===
   time (s)            : 0.82
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 142
   states saved        : 114
   state matches       : 1
   transitions         : 142
   trace steps         : 114
   valid calls         : 1
   provers             : z3, cvc4, cvc3
   prover calls        : 0

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

=== Command ===
civl verify -enablePrintf=false locksGood.cvl 

=== Stats ===
   time (s)            : 0.69
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 15
   states saved        : 4
   state matches       : 2
   transitions         : 16
   trace steps         : 5
   valid calls         : 8
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false mpi-pthreads.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 106:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at mpi-pthreads.cvl:43.2-10 "$waitall":
A deadlock is possible:
  Path condition: 0 <= SIZEOF_INT+-1
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): false
process p3 (id=3): false
process p4 (id=4): false
process p5 (id=5): terminated
process p6 (id=6): false

Call stacks:

process p0 (id=0):
  _CIVL_system at mpi-pthreads.cvl:43.2-10 "$waitall"

process p1 (id=1):
  MPI_Process at mpi-pthreads.cvl:34.2-10 "$waitall"

process p2 (id=2):
  MPI_Process at mpi-pthreads.cvl:34.2-10 "$waitall"

process p3 (id=3):
  Thread at mpi-pthreads.cvl:26.37-50 "$comm_dequeue"

process p4 (id=4):
  Thread at mpi-pthreads.cvl:26.37-50 "$comm_dequeue"

process p5 (id=5):
  terminated

process p6 (id=6):
  Thread at mpi-pthreads.cvl:24.37-50 "$comm_dequeue"

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

=== Command ===
civl verify -enablePrintf=false mpi-pthreads.cvl 

=== Stats ===
   time (s)            : 1.64
   memory (bytes)      : 163053568
   max process count   : 7
   states              : 921
   states saved        : 594
   state matches       : 46
   transitions         : 966
   trace steps         : 635
   valid calls         : 9580
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/mpi-pthreads_log.txt
civl verify -enablePrintf=false readerWriter.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false readerWriter.cvl 

=== Stats ===
   time (s)            : 1.37
   memory (bytes)      : 128974848
   max process count   : 7
   states              : 1092
   states saved        : 438
   state matches       : 652
   transitions         : 1743
   trace steps         : 1089
   valid calls         : 7032
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -deadlock=potential -inputNPROCS_BOUND=10 -inputN_BOUND=5 ring.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -deadlock=potential -inputNPROCS_BOUND=10 -inputN_BOUND=5 ring.cvl 

=== Stats ===
   time (s)            : 6.46
   memory (bytes)      : 375390208
   max process count   : 11
   states              : 11874
   states saved        : 8170
   state matches       : 0
   transitions         : 11873
   trace steps         : 7059
   valid calls         : 31147
   provers             : z3, cvc4, cvc3
   prover calls        : 44

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -deadlock=potential -inputNPROCS=3 ring1.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -deadlock=potential -inputNPROCS=3 ring1.cvl 

=== Stats ===
   time (s)            : 1.24
   memory (bytes)      : 128974848
   max process count   : 4
   states              : 127
   states saved        : 76
   state matches       : 2
   transitions         : 128
   trace steps         : 70
   valid calls         : 399
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -deadlock=potential -inputNPROCS=3 ring1Bad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 29:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at mp_root.cvh:16.4-9 "$wait" included from ring1Bad.cvl:7.9-22 ""mp_root.cvh"":
A potential or absolute deadlock is possible:
  Path condition: 0 <= SIZEOF_REAL+-1
  Enabling predicate: false
ProcessState 0: at location 31, mp_root.cvh:16.4-9 "$wait" included from ring1Bad.cvl:7.9-22 ""mp_root.cvh""
  Enabling predicate: false
ProcessState 1: at location 42, mp_proc.cvh:3.4-17 "$comm_enqueue" included from ring1Bad.cvl:10.11-24 ""mp_proc.cvh""
  Enabling predicate: true
ProcessState 2: at location 42, mp_proc.cvh:3.4-17 "$comm_enqueue" included from ring1Bad.cvl:10.11-24 ""mp_proc.cvh""
  Enabling predicate: true
ProcessState 3: at location 42, mp_proc.cvh:3.4-17 "$comm_enqueue" included from ring1Bad.cvl:10.11-24 ""mp_proc.cvh""
  Enabling predicate: true

Call stacks:

process p0 (id=0):
  finalize at mp_root.cvh:16.4-9 "$wait" included from ring1Bad.cvl:7.9-22 ""mp_root.cvh"" called from
  _CIVL_system at mp_root.cvh:24.4-12 "finalize" included from ring1Bad.cvl:7.9-22 ""mp_root.cvh""

process p1 (id=1):
  send at mp_proc.cvh:3.4-17 "$comm_enqueue" included from ring1Bad.cvl:10.11-24 ""mp_proc.cvh"" called from
  MPI_Process at ring1Bad.cvl:14.2-6 "send"

process p2 (id=2):
  send at mp_proc.cvh:3.4-17 "$comm_enqueue" included from ring1Bad.cvl:10.11-24 ""mp_proc.cvh"" called from
  MPI_Process at ring1Bad.cvl:14.2-6 "send"

process p3 (id=3):
  send at mp_proc.cvh:3.4-17 "$comm_enqueue" included from ring1Bad.cvl:10.11-24 ""mp_proc.cvh"" called from
  MPI_Process at ring1Bad.cvl:14.2-6 "send"

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

=== Command ===
civl verify -enablePrintf=false -deadlock=potential -inputNPROCS=3 ring1Bad.cvl 

=== Stats ===
   time (s)            : 1.1
   memory (bytes)      : 128974848
   max process count   : 4
   states              : 60
   states saved        : 32
   state matches       : 0
   transitions         : 59
   trace steps         : 28
   valid calls         : 119
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/ring1Bad_log.txt
civl verify -enablePrintf=false -inputNPROCS=3 -deadlock=potential ring2.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -inputNPROCS=3 -deadlock=potential ring2.cvl 

=== Stats ===
   time (s)            : 1.6
   memory (bytes)      : 163053568
   max process count   : 4
   states              : 228
   states saved        : 163
   state matches       : 2
   transitions         : 229
   trace steps         : 154
   valid calls         : 891
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -inputNPROCS=3 -deadlock=potential ring2Bad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 59:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at mp_root2.cvh:67.4-9 "$wait" included from ring2Bad.cvl:8.9-23 ""mp_root2.cvh"":
A potential or absolute deadlock is possible:
  Path condition: 0 <= SIZEOF_REAL+-1
  Enabling predicate: false
ProcessState 0: at location 41, mp_root2.cvh:67.4-9 "$wait" included from ring2Bad.cvl:8.9-23 ""mp_root2.cvh""
  Enabling predicate: false
ProcessState 1: at location 72, mp_proc2.cvh:38.4-17 "$comm_enqueue" included from ring2Bad.cvl:11.9-23 ""mp_proc2.cvh""
  Enabling predicate: true
ProcessState 2: at location 72, mp_proc2.cvh:38.4-17 "$comm_enqueue" included from ring2Bad.cvl:11.9-23 ""mp_proc2.cvh""
  Enabling predicate: true
ProcessState 3: at location 72, mp_proc2.cvh:38.4-17 "$comm_enqueue" included from ring2Bad.cvl:11.9-23 ""mp_proc2.cvh""
  Enabling predicate: true

Call stacks:

process p0 (id=0):
  finalize at mp_root2.cvh:67.4-9 "$wait" included from ring2Bad.cvl:8.9-23 ""mp_root2.cvh"" called from
  _CIVL_system at mp_root2.cvh:73.2-10 "finalize" included from ring2Bad.cvl:8.9-23 ""mp_root2.cvh""

process p1 (id=1):
  MPI_Send at mp_proc2.cvh:38.4-17 "$comm_enqueue" included from ring2Bad.cvl:11.9-23 ""mp_proc2.cvh"" called from
  MPI_Process at ring2Bad.cvl:23.2-10 "MPI_Send"

process p2 (id=2):
  MPI_Send at mp_proc2.cvh:38.4-17 "$comm_enqueue" included from ring2Bad.cvl:11.9-23 ""mp_proc2.cvh"" called from
  MPI_Process at ring2Bad.cvl:23.2-10 "MPI_Send"

process p3 (id=3):
  MPI_Send at mp_proc2.cvh:38.4-17 "$comm_enqueue" included from ring2Bad.cvl:11.9-23 ""mp_proc2.cvh"" called from
  MPI_Process at ring2Bad.cvl:23.2-10 "MPI_Send"

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

=== Command ===
civl verify -enablePrintf=false -inputNPROCS=3 -deadlock=potential ring2Bad.cvl 

=== Stats ===
   time (s)            : 1.43
   memory (bytes)      : 163053568
   max process count   : 4
   states              : 92
   states saved        : 62
   state matches       : 0
   transitions         : 91
   trace steps         : 58
   valid calls         : 250
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/ring2Bad_log.txt
civl verify -enablePrintf=false -deadlock=potential ring3.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -deadlock=potential ring3.cvl 

=== Stats ===
   time (s)            : 1.2
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 69
   states saved        : 51
   state matches       : 1
   transitions         : 69
   trace steps         : 42
   valid calls         : 323
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -deadlock=potential ring3Bad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 16:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at ring3Bad.cvl:30.52-53 ";":
A potential or absolute deadlock is possible:
  Path condition: 0 <= SIZEOF_INT+-1
  Enabling predicate: false
ProcessState 0: at location 2, ring3Bad.cvl:30.52-53 ";"
  Enabling predicate: false
ProcessState 1: at location 24, ring3Bad.cvl:20.2-15 "$comm_enqueue"
  Enabling predicate: true
ProcessState 2: at location 24, ring3Bad.cvl:20.2-15 "$comm_enqueue"
  Enabling predicate: true

Call stacks:

process p0 (id=0):
  _CIVL_system at ring3Bad.cvl:30.52-53 ";"

process p1 (id=1):
  MPI_Process at ring3Bad.cvl:20.2-15 "$comm_enqueue"

process p2 (id=2):
  MPI_Process at ring3Bad.cvl:20.2-15 "$comm_enqueue"

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

=== Command ===
civl verify -enablePrintf=false -deadlock=potential ring3Bad.cvl 

=== Stats ===
   time (s)            : 1.46
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 33
   states saved        : 22
   state matches       : 0
   transitions         : 32
   trace steps         : 15
   valid calls         : 111
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/ring3Bad_log.txt
civl verify -enablePrintf=false -inputN=10 spawn.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -inputN=10 spawn.cvl 

=== Stats ===
   time (s)            : 0.81
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 63
   states saved        : 52
   state matches       : 0
   transitions         : 62
   trace steps         : 51
   valid calls         : 2
   provers             : z3, cvc4, cvc3
   prover calls        : 0

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

=== Command ===
civl verify -enablePrintf=false -inputN=10 spawn2.cvl 

=== Stats ===
   time (s)            : 0.86
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 717
   states saved        : 423
   state matches       : 121
   transitions         : 837
   trace steps         : 543
   valid calls         : 1
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -inputN=10 spawnBad.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 8:
CIVL execution error in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE) 
at spawnBad.cvl:23.2-19 "$assert((s1==s2))":

Context: true

Assertion: $assert((s1==s2))
-> 1==0
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at spawnBad.cvl:23.2-9 "$assert"

process p1 (id=1):
  f1 at spawnBad.cvl:11.26-28 "s1"

process p2 (id=2):
  f2 at spawnBad.cvl:15.2-4 "s2"

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

=== Command ===
civl verify -enablePrintf=false -inputN=10 spawnBad.cvl 

=== Stats ===
   time (s)            : 0.91
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 727
   states saved        : 429
   state matches       : 123
   transitions         : 850
   trace steps         : 551
   valid calls         : 5
   provers             : z3, cvc4, cvc3
   prover calls        : 0

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

=== Command ===
civl verify -enablePrintf=false two_lock_queue.cvl 

=== Stats ===
   time (s)            : 1.15
   memory (bytes)      : 128974848
   max process count   : 3
   states              : 109
   states saved        : 93
   state matches       : 1
   transitions         : 109
   trace steps         : 88
   valid calls         : 52
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false waitSelf.cvl
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 1:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at waitSelf.cvl:4.1-6 "$wait":
A deadlock is possible:
  Path condition: true
  Enabling predicate: false
process p0 (id=0): false

Call stacks:

process p0 (id=0):
  _CIVL_system at waitSelf.cvl:4.1-6 "$wait"

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

=== Command ===
civl verify -enablePrintf=false waitSelf.cvl 

=== Stats ===
   time (s)            : 0.76
   memory (bytes)      : 128974848
   max process count   : 0
   states              : 1
   states saved        : 1
   state matches       : 0
   transitions         : 0
   trace steps         : 0
   valid calls         : 1
   provers             : z3, cvc4, cvc3
   prover calls        : 0

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

=== Command ===
civl verify -enablePrintf=false wildcard.cvl 

=== Stats ===
   time (s)            : 3.72
   memory (bytes)      : 231211008
   max process count   : 6
   states              : 1607
   states saved        : 1090
   state matches       : 23
   transitions         : 1629
   trace steps         : 1056
   valid calls         : 6564
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false wildcardBad.c
CIVL vpre-1.0 of 2015-02-09 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 196:
CIVL execution error in  (kind: DEADLOCK, certainty: PROVEABLE) 
at MPItoCIVLTransformer:0.-1-19 "$mpi_procs, _NPROCS\n" inserted by MPItoCIVLTransformer.function call$waitall before op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from stdio.cvl:11.10-21 "<civlc.cvh>":
A deadlock is possible:
  Path condition: (0 <= SIZEOF_INT+-1) && (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):
  _CIVL_system at MPItoCIVLTransformer:0.-1-19 "$mpi_procs, _NPROCS\n" inserted by MPItoCIVLTransformer.function call$waitall before op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from stdio.cvl:11.10-21 "<civlc.cvh>"

process p1 (id=1):
  CMPI_Recv at civl-mpi.cvl:143.18-31 "$comm_dequeue" called from
  MPI_Recv at mpi.cvl:84.9-18 "CMPI_Recv" called from
  $mpi_main at wildcardBad.c:23.4-12 "MPI_Recv" called from
  MPI_Process at MPItoCIVLTransformer:0.-1 "" inserted by MPItoCIVLTransformer.function call $mpi_main before op.h:22.1-10 "Operation" included from civlc.cvh:12.9-15 "<op.h>" included from stdio.cvl:11.10-21 "<civlc.cvh>"

process p2 (id=2):
  terminated

process p3 (id=3):
  terminated

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

=== Command ===
civl verify -enablePrintf=false wildcardBad.c 

=== Stats ===
   time (s)            : 3.11
   memory (bytes)      : 231211008
   max process count   : 4
   states              : 334
   states saved        : 202
   state matches       : 0
   transitions         : 333
   trace steps         : 195
   valid calls         : 1390
   provers             : z3, cvc4, cvc3
   prover calls        : 4

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