civl verify -enablePrintf=false 2dpointerTest.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false 2dpointerTest.cvl 

=== Stats ===
   time (s)            : 0.66
   memory (bytes)      : 514850816
   max process count   : 3
   states              : 51
   states saved        : 32
   state matches       : 0
   transitions         : 50
   trace steps         : 23
   valid calls         : 138
   provers             : z3, cvc4, cvc3
   prover calls        : 3

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false abstractFun.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.82
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 13
   states saved        : 6
   state matches       : 0
   transitions         : 12
   trace steps         : 4
   valid calls         : 3
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false abstractFunNoArg.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
civl verify -enablePrintf=false arrayDefProblem.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.78
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 7
   states saved        : 5
   state matches       : 0
   transitions         : 6
   trace steps         : 4
   valid calls         : 6
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false arrayLiteral.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false arrayPointer.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.55
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 7
   states saved        : 5
   state matches       : 0
   transitions         : 6
   trace steps         : 4
   valid calls         : 8
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false arrays.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.57
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 12
   states saved        : 9
   state matches       : 0
   transitions         : 11
   trace steps         : 8
   valid calls         : 47
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false assertNonNullPointer.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.79
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 4
   states saved        : 3
   state matches       : 0
   transitions         : 3
   trace steps         : 2
   valid calls         : 7
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false assertNullPointer.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 2:
CIVL execution violation in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at assertNullPointer.cvl:10.2-14 "$assert((p))":


Context: true

Assertion: $assert((p!=(($real)*) 0))
-> NULL!=(($real)*)0
-> NULL!=NULL
-> false

Call stacks:

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

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/assertNullPointer_log.txt
civl verify -enablePrintf=false assertPrintf.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
2 is smaller than 10!

Violation 0 encountered at depth 3:
CIVL execution violation in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at assertPrintf.cvl:13.2-48 "$assert(b > a,  ... )":


Context: true

Assertion: $assert((a<b), &((_anon_1)[0]), b, a)
-> 10<2
-> false

Call stacks:

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

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/assertPrintf_log.txt
civl verify -enablePrintf=false assignInput.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
civl verify -enablePrintf=false assignIntWtReal.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false assume.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false atomChooseBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 1:
CIVL execution violation in p0 (id = 0) (kind: OTHER, certainty: CONCRETE)
at atomChooseBad.cvl:13.4-11 "$choose":
Non-determinism is encountered in $atom block.

Call stacks:

process p0 (id=0):
  _CIVL_system at atomChooseBad.cvl:13.4-11 "$choose"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/atomChooseBad_log.txt
civl verify -enablePrintf=false atomicBlockedResume.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.57
   memory (bytes)      : 514850816
   max process count   : 3
   states              : 40
   states saved        : 20
   state matches       : 2
   transitions         : 41
   trace steps         : 21
   valid calls         : 94
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -inputB=3 atomicStatement.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -inputB=3 atomicStatement.cvl 

=== Stats ===
   time (s)            : 0.62
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 23
   states saved        : 7
   state matches       : 1
   transitions         : 23
   trace steps         : 6
   valid calls         : 21
   provers             : z3, cvc4, cvc3
   prover calls        : 3

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -inputN=3 atomicWait.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -inputN=3 atomicWait.cvl 

=== Stats ===
   time (s)            : 0.58
   memory (bytes)      : 514850816
   max process count   : 4
   states              : 61
   states saved        : 18
   state matches       : 5
   transitions         : 65
   trace steps         : 22
   valid calls         : 67
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false atomStatement.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.71
   memory (bytes)      : 514850816
   max process count   : 6
   states              : 806
   states saved        : 129
   state matches       : 80
   transitions         : 885
   trace steps         : 208
   valid calls         : 345
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false atomWaitBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 1:
CIVL execution violation in p0 (id = 0) (kind: OTHER, certainty: CONCRETE)
at atomWaitBad.cvl:19.4-9 "$wait":
Blocked location is encountered in $atom block.

Call stacks:

process p0 (id=0):
  _CIVL_system at atomWaitBad.cvl:19.4-9 "$wait"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/atomWaitBad_log.txt
civl verify -enablePrintf=false badGuard.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 1:
CIVL execution violation in p0 (id = 0) (kind: DIVISION_BY_ZERO, certainty: PROVEABLE)
at badGuard.cvl:14.10-13 "x/y":
Division by zero

Call stacks:

process p0 (id=0):
  _CIVL_system at badGuard.cvl:13.2-9 "$choose"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/badGuard_log.txt
civl verify -enablePrintf=false bitwise.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false break.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.56
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 100
   states saved        : 39
   state matches       : 0
   transitions         : 99
   trace steps         : 38
   valid calls         : 2
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false bundleArray.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.6
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 10
   states saved        : 7
   state matches       : 0
   transitions         : 9
   trace steps         : 5
   valid calls         : 45
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false bundleConcrete.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.59
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 18
   states saved        : 8
   state matches       : 0
   transitions         : 17
   trace steps         : 6
   valid calls         : 66
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false bundleSize.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.59
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 8
   states saved        : 4
   state matches       : 0
   transitions         : 7
   trace steps         : 2
   valid calls         : 14
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false bundleStruct.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.59
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 10
   states saved        : 9
   state matches       : 0
   transitions         : 9
   trace steps         : 7
   valid calls         : 6
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false bundleTest.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.92
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 559
   states saved        : 135
   state matches       : 0
   transitions         : 558
   trace steps         : 126
   valid calls         : 1695
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false bundleTestBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 63:
CIVL execution violation in p0(id=0) (kind: OUT_OF_BOUNDS, certainty: PROVEABLE)
at bundleTestBad.cvl:20.2-36 "$bundle_unpack(bun, &a4d[1 ... )":
Pointer addition results in an index out of bound error on A allocated sequence of memory space: (int[2][2][2][2])X_s1v3p0
Original pointer: &<d1>a4d[1][0][1][0]
Pointer addtion offset: 8

Call stacks:

process p0 (id=0):
  _CIVL_system at bundleTestBad.cvl:20.2-16 "$bundle_unpack"

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

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

=== Stats ===
   time (s)            : 0.68
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 367
   states saved        : 64
   state matches       : 0
   transitions         : 367
   trace steps         : 62
   valid calls         : 58
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/bundleTestBad_log.txt
civl verify -enablePrintf=false cast.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false char.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false choose.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false choose_int.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.78
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 22
   states saved        : 7
   state matches       : 4
   transitions         : 25
   trace steps         : 10
   valid calls         : 5
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false civlfor.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.85
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 281
   states saved        : 106
   state matches       : 0
   transitions         : 280
   trace steps         : 105
   valid calls         : 12
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false civlParfor.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 1.23
   memory (bytes)      : 514850816
   max process count   : 9
   states              : 1352
   states saved        : 288
   state matches       : 769
   transitions         : 2120
   trace steps         : 1056
   valid calls         : 10214
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false -inputNB=5 civlPragma.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

=== Command ===
civl verify -enablePrintf=false -inputNB=5 civlPragma.cvl 

=== Stats ===
   time (s)            : 0.76
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 42
   states saved        : 15
   state matches       : 0
   transitions         : 41
   trace steps         : 7
   valid calls         : 73
   provers             : z3, cvc4, cvc3
   prover calls        : 14

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false comma.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 5.29
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 710
   states saved        : 402
   state matches       : 0
   transitions         : 709
   trace steps         : 202
   valid calls         : 1513
   provers             : z3, cvc4, cvc3
   prover calls        : 398

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false compare.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false conditionalExpression.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.6
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 98
   states saved        : 26
   state matches       : 0
   transitions         : 97
   trace steps         : 25
   valid calls         : 36
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false continue.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.64
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 776
   states saved        : 207
   state matches       : 0
   transitions         : 775
   trace steps         : 206
   valid calls         : 97
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false duffs.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.64
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 76
   states saved        : 53
   state matches       : 0
   transitions         : 75
   trace steps         : 52
   valid calls         : 199
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false dynamicStruct.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.59
   memory (bytes)      : 514850816
   max process count   : 4
   states              : 65
   states saved        : 26
   state matches       : 0
   transitions         : 64
   trace steps         : 25
   valid calls         : 12
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false emptyWhen.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false enum1.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.56
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 8
   states saved        : 7
   state matches       : 0
   transitions         : 7
   trace steps         : 6
   valid calls         : 2
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false enum2.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.56
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 17
   states saved        : 2
   state matches       : 0
   transitions         : 16
   trace steps         : 1
   valid calls         : 7
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false for.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.49
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 79
   states saved        : 44
   state matches       : 0
   transitions         : 78
   trace steps         : 43
   valid calls         : 0
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false functionBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 3:
CIVL execution violation in p0 (id = 0) (kind: OTHER, certainty: PROVEABLE)
at functionBad.cvl:18.2-13 "int a = f()":
functionBad.cvl:18.2-13 "int a = f()" :  Attempt to use the return value of function f when f has returned without a return value.

Call stacks:

process p0 (id=0):
  _CIVL_system at functionBad.cvl:18.10-11 "f"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/functionBad_log.txt
civl verify -enablePrintf=false functionPointer.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.96
   memory (bytes)      : 514850816
   max process count   : 4
   states              : 411
   states saved        : 227
   state matches       : 53
   transitions         : 463
   trace steps         : 279
   valid calls         : 983
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false functionPrototype.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false functionPrototypeBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
civl verify -enablePrintf=false implies.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.64
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 37
   states saved        : 14
   state matches       : 0
   transitions         : 36
   trace steps         : 12
   valid calls         : 26
   provers             : z3, cvc4, cvc3
   prover calls        : 5

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false include1.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 2:
CIVL execution violation in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at include3.cvl:4.2-15 "$assert(n>=0)" included from include2.cvl:1.9-23 ""include3.cvl"" included from include1.cvl:2.9-23 ""include2.cvl"":

Input variables:
n=X0

Context: true

Assertion: $assert((0<=n))
-> 0<=X0

Call stacks:

process p0 (id=0):
  f2 at include3.cvl:4.2-9 "$assert" included from include2.cvl:1.9-23 ""include3.cvl"" included from include1.cvl:2.9-23 ""include2.cvl"" called from
  _CIVL_system at include1.cvl:7.2-4 "f2"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/include1_log.txt
civl verify -enablePrintf=false include2.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
civl verify -enablePrintf=false include3.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
civl verify -enablePrintf=false inputBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 4:
CIVL execution violation in p0 (id = 0) (kind: INPUT_WRITE, certainty: PROVEABLE)
at inputBad.cvl:15.2-5 "*ka":
Attempt to write to input variable k

Call stacks:

process p0 (id=0):
  _CIVL_system at inputBad.cvl:15.2-5 "*ka"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/inputBad_log.txt
civl verify -enablePrintf=false int2char.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.86
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 17
   states saved        : 15
   state matches       : 0
   transitions         : 16
   trace steps         : 12
   valid calls         : 95
   provers             : z3, cvc4, cvc3
   prover calls        : 4

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false int2charBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 5:
CIVL execution violation in p0(id=0) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at int2charBad.cvl:15.2-27 "$assert((pc[0] == ... )":

Input variables:
num1=X0
num2=X1

Context: 0<=SIZEOF_CHAR+-1 && 0<=-1*X0+254 && 0<=X0+-1 && 0<=-1*X1+254 && 0<=X1+-1

Assertion: $assert((*((pc+0))==*((pc+1))))
-> *(&<d0>heap.malloc0[0][0]+0)==*(&<d0>heap.malloc0[0][0]+1)
-> int2char(X0)==int2char(X1)

Call stacks:

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

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

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

=== Stats ===
   time (s)            : 0.92
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 8
   states saved        : 7
   state matches       : 0
   transitions         : 8
   trace steps         : 4
   valid calls         : 59
   provers             : z3, cvc4, cvc3
   prover calls        : 7

=== Result ===
The program MAY NOT be correct.  See CIVLREP/int2charBad_log.txt
civl verify -enablePrintf=false int2charBad2.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Error: This feature is not yet implemented: Converting integer whose value is larger than UCHAR_MAX or is less than UCHAR_MIN to char type

civl verify -enablePrintf=false int2float.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false intToBool.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.78
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 6
   states saved        : 4
   state matches       : 0
   transitions         : 5
   trace steps         : 3
   valid calls         : 0
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false linkedList.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.98
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 138
   states saved        : 133
   state matches       : 0
   transitions         : 137
   trace steps         : 118
   valid calls         : 236
   provers             : z3, cvc4, cvc3
   prover calls        : 20

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false malloc.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.59
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 7
   states saved        : 7
   state matches       : 0
   transitions         : 6
   trace steps         : 5
   valid calls         : 31
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false mallocBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 3:
CIVL execution violation in p0 (id = 0) (kind: DEREFERENCE, certainty: PROVEABLE)
at mallocBad.cvl:11.11-15 "p[4]":
Attempt to dereference a pointer that refers to a memory space that is already deallocated

Call stacks:

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

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

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

=== Stats ===
   time (s)            : 0.61
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 3
   states saved        : 4
   state matches       : 0
   transitions         : 3
   trace steps         : 2
   valid calls         : 7
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/mallocBad_log.txt
civl verify -enablePrintf=false mallocBad2.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 1:
CIVL execution violation in p0 (id = 0) (kind: UNDEFINED_VALUE, certainty: PROVEABLE)
at mallocBad2.cvl:10.2-3 "p":
Attempt to read uninitialized variable p

Call stacks:

process p0 (id=0):
  _CIVL_system at mallocBad2.cvl:10.2-6 "p[4]"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/mallocBad2_log.txt
civl verify -enablePrintf=false memLeak.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl
civl verify -enablePrintf=false memoryLeak.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 20:
CIVL execution violation in p1 (id = 1) (kind: MEMORY_LEAK, certainty: CONCRETE)
at memoryLeak.cvl:10.14-21.1 "{\n  int * p  ... }":
The dyscope d3(id=4) has a non-empty heap upon termination.
heap
| objects of malloc 1 at memoryLeak.cvl:11.2-47 "int * p = ( ... )":
| | 0: (int[1]){10}

Call stacks:

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

process p1 (id=1):
  terminated

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

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

=== Stats ===
   time (s)            : 0.64
   memory (bytes)      : 514850816
   max process count   : 2
   states              : 33
   states saved        : 27
   state matches       : 0
   transitions         : 33
   trace steps         : 19
   valid calls         : 14
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The program MAY NOT be correct.  See CIVLREP/memoryLeak_log.txt
civl verify -enablePrintf=false minimal.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false nonbooleanCondition.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.59
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 15
   states saved        : 6
   state matches       : 0
   transitions         : 14
   trace steps         : 5
   valid calls         : 9
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false noopBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 2:
CIVL execution violation in p0 (id = 0) (kind: DIVISION_BY_ZERO, certainty: PROVEABLE)
at noopBad.cvl:10.2-8 "a[0]/n":
Division by zero

Call stacks:

process p0 (id=0):
  _CIVL_system at noopBad.cvl:10.2-3 "a"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/noopBad_log.txt
civl verify -enablePrintf=false not.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false null.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false outputBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 2:
CIVL execution violation in p0 (id = 0) (kind: OUTPUT_READ, certainty: PROVEABLE)
at outputBad.cvl:14.8-9 "p":
Attempt to read output variable k

Call stacks:

process p0 (id=0):
  _CIVL_system at outputBad.cvl:14.2-4 "ka"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/outputBad_log.txt
civl verify -enablePrintf=false pointerAdd.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 2.14
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 4058
   states saved        : 1493
   state matches       : 0
   transitions         : 4057
   trace steps         : 1369
   valid calls         : 18505
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false pointerAdd1.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false pointerAdd2.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 4.94
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 1007
   states saved        : 540
   state matches       : 0
   transitions         : 1006
   trace steps         : 388
   valid calls         : 5502
   provers             : z3, cvc4, cvc3
   prover calls        : 327

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false pointerAddBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 2:
CIVL execution violation in p0 (id = 0) (kind: DEREFERENCE, certainty: PROVEABLE)
at pointerAddBad.cvl:9.10-30 "(&a[0][0] ... )":
Illegal pointer dereference: Array index out of bounds in method arrayRead.
array: X0[9][9]
extent: 10
index: 10

Call stacks:

process p0 (id=0):
  _CIVL_system at pointerAddBad.cvl:8.0-6 "printf"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/pointerAddBad_log.txt
civl verify -enablePrintf=false pointerAddBad2.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 112:
CIVL execution violation in p0 (id = 0) (kind: DEREFERENCE, certainty: PROVEABLE)
at pointerAddBad2.cvl:16.9-24 "(&p[0][0] ... )":
Illegal pointer dereference: Array index out of bounds in method arrayRead.
array: (int[10])<0,0,0,0,0,0,0,0,0,0>
extent: 10
index: 10

Call stacks:

process p0 (id=0):
  _CIVL_system at pointerAddBad2.cvl:16.2-5 "ret"

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

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

=== Stats ===
   time (s)            : 0.99
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 354
   states saved        : 123
   state matches       : 0
   transitions         : 354
   trace steps         : 111
   valid calls         : 806
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The program MAY NOT be correct.  See CIVLREP/pointerAddBad2_log.txt
civl verify -enablePrintf=false pointers.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.64
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 46
   states saved        : 34
   state matches       : 0
   transitions         : 45
   trace steps         : 30
   valid calls         : 33
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false pointerSubtraction.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.8
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 37
   states saved        : 23
   state matches       : 0
   transitions         : 36
   trace steps         : 18
   valid calls         : 178
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false pointerSubtractionBad.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 3:
CIVL execution violation in p0 (id = 0) (kind: POINTER, certainty: PROVEABLE)
at pointerSubtractionBad.cvl:11.9-14 "p - b":
Operands of pointer subtraction point to the same obejct

Call stacks:

process p0 (id=0):
  _CIVL_system at pointerSubtractionBad.cvl:11.2-6 "diff"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/pointerSubtractionBad_log.txt
civl verify -enablePrintf=false pointerSubtractionBad2.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 5:
CIVL execution violation in p0 (id = 0) (kind: POINTER, certainty: PROVEABLE)
at pointerSubtractionBad2.cvl:13.9-20 "x[1] - x[ ... ]":
Operands of pointer subtraction point to different heap obejcts

Call stacks:

process p0 (id=0):
  _CIVL_system at pointerSubtractionBad2.cvl:13.2-6 "diff"

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

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

=== Stats ===
   time (s)            : 0.78
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 13
   states saved        : 9
   state matches       : 0
   transitions         : 13
   trace steps         : 4
   valid calls         : 23
   provers             : z3, cvc4, cvc3
   prover calls        : 2

=== Result ===
The program MAY NOT be correct.  See CIVLREP/pointerSubtractionBad2_log.txt
civl verify -enablePrintf=false -procBound=10 procBound.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 11:
CIVL execution violation in p1(id=1) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at procBound.cvl:4.2-17 "$assert($false)":


Context: true

Assertion: $assert(false)
-> false

Call stacks:

process p0 (id=0):
  _CIVL_system at procBound.cvl:8.15-21 "$spawn"

process p1 (id=1):
  f at procBound.cvl:4.2-9 "$assert"

process p2 (id=2):
  f at procBound.cvl:4.2-9 "$assert"

process p3 (id=3):
  f at procBound.cvl:4.2-9 "$assert"

process p4 (id=4):
  f at procBound.cvl:4.2-9 "$assert"

process p5 (id=5):
  f at procBound.cvl:4.2-9 "$assert"

process p6 (id=6):
  f at procBound.cvl:4.2-9 "$assert"

process p7 (id=7):
  f at procBound.cvl:4.2-9 "$assert"

process p8 (id=8):
  f at procBound.cvl:4.2-9 "$assert"

process p9 (id=9):
  f at procBound.cvl:4.2-9 "$assert"

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

=== Command ===
civl verify -enablePrintf=false -procBound=10 procBound.cvl 

=== Stats ===
   time (s)            : 0.57
   memory (bytes)      : 514850816
   max process count   : 10
   states              : 20
   states saved        : 11
   state matches       : 0
   transitions         : 20
   trace steps         : 10
   valid calls         : 2
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/procBound_log.txt
civl verify -enablePrintf=false processLeak.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 2:
CIVL execution violation in p0 (id = 0) (kind: PROCESS_LEAK, certainty: CONCRETE)
at processLeak.cvl:20.0-1 "}":
Attempt to terminate the main process while process 1(process<1>) is still running

Call stacks:

process p0 (id=0):
  _CIVL_system at processLeak.cvl:20.0-1 "}"

process p1 (id=1):
  process at processLeak.cvl:13.28-29 ";"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/processLeak_log.txt
civl verify -enablePrintf=false procNull.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.77
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 6
   states saved        : 4
   state matches       : 0
   transitions         : 5
   trace steps         : 3
   valid calls         : 0
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false quantifiers.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.73
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 25
   states saved        : 7
   state matches       : 0
   transitions         : 24
   trace steps         : 6
   valid calls         : 39
   provers             : z3, cvc4, cvc3
   prover calls        : 11

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false removedHeapPointer.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 9:
CIVL execution violation in p2 (id = 1) (kind: DEREFERENCE, certainty: PROVEABLE)
at removedHeapPointer.cvl:23.2-5 "*gp":
Attempt to dereference a pointer that refers to a memory space that is already deallocated

Call stacks:

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

process p2 (id=1):
  goo at removedHeapPointer.cvl:23.2-5 "*gp"

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

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

=== Stats ===
   time (s)            : 0.61
   memory (bytes)      : 514850816
   max process count   : 3
   states              : 13
   states saved        : 10
   state matches       : 0
   transitions         : 13
   trace steps         : 8
   valid calls         : 3
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The program MAY NOT be correct.  See CIVLREP/removedHeapPointer_log.txt
civl verify -enablePrintf=false scopeOperators.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.89
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 40
   states saved        : 22
   state matches       : 0
   transitions         : 39
   trace steps         : 21
   valid calls         : 41
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false scoping.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 2:
CIVL execution violation in p0 (id = 0) (kind: MEMORY_LEAK, certainty: CONCRETE)
at scoping.cvl:11.2-14.3 "{\n     p = (int ... }":
The dyscope d2(id=1) has a non-empty heap upon termination.
heap
| objects of malloc 0 at scoping.cvl:12.5-44 "p = (int *) ... )":
| | 0: (int[1])Hop0s1f0o0

Call stacks:

process p0 (id=0):
  _CIVL_system at scoping.cvl:21.5-6 "q"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/scoping_log.txt
civl verify -enablePrintf=false self.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.55
   memory (bytes)      : 514850816
   max process count   : 2
   states              : 9
   states saved        : 6
   state matches       : 0
   transitions         : 8
   trace steps         : 5
   valid calls         : 1
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false sideEffectLoop.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.8
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 29
   states saved        : 14
   state matches       : 0
   transitions         : 28
   trace steps         : 13
   valid calls         : 1
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false sideEffects.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.56
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 17
   states saved        : 2
   state matches       : 0
   transitions         : 16
   trace steps         : 1
   valid calls         : 3
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false sizeof.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false spawnFoo.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 2:
CIVL execution violation in p1(id=1) (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
at spawnFoo.cvl:4.2-19 "$assert(($false))":


Context: true

Assertion: $assert(false)
-> false

Call stacks:

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

process p1 (id=1):
  foo at spawnFoo.cvl:4.2-9 "$assert"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/spawnFoo_log.txt
civl verify -enablePrintf=false stringTest.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.85
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 22
   states saved        : 23
   state matches       : 0
   transitions         : 21
   trace steps         : 18
   valid calls         : 46
   provers             : z3, cvc4, cvc3
   prover calls        : 1

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false struct.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.56
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 10
   states saved        : 3
   state matches       : 0
   transitions         : 9
   trace steps         : 2
   valid calls         : 13
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false structArray.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.57
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 19
   states saved        : 9
   state matches       : 0
   transitions         : 18
   trace steps         : 8
   valid calls         : 26
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false structStruct.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.56
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 9
   states saved        : 5
   state matches       : 0
   transitions         : 8
   trace steps         : 4
   valid calls         : 26
   provers             : z3, cvc4, cvc3
   prover calls        : 0

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false switch.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

=== Stats ===
   time (s)            : 0.86
   memory (bytes)      : 514850816
   max process count   : 1
   states              : 18
   states saved        : 21
   state matches       : 0
   transitions         : 17
   trace steps         : 14
   valid calls         : 55
   provers             : z3, cvc4, cvc3
   prover calls        : 18

=== Result ===
The standard properties hold for all executions.
civl verify -enablePrintf=false undefHeapPointer.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 2:
CIVL execution violation in p0 (id = 0) (kind: UNDEFINED_VALUE, certainty: PROVEABLE)
at undefHeapPointer.cvl:12.6-13 "n->next":
Attempt to use undefined pointer

Call stacks:

process p0 (id=0):
  _CIVL_system at undefHeapPointer.cvl:12.2-4 "if"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/undefHeapPointer_log.txt
civl verify -enablePrintf=false undefPointer.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 1:
CIVL execution violation in p0 (id = 0) (kind: UNDEFINED_VALUE, certainty: PROVEABLE)
at undefPointer.cvl:11.6-12 "n.next":
Attempt to use undefined pointer

Call stacks:

process p0 (id=0):
  _CIVL_system at undefPointer.cvl:11.2-4 "if"

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

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

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

=== Result ===
The program MAY NOT be correct.  See CIVLREP/undefPointer_log.txt
civl verify -enablePrintf=false union.cvl
CIVL v1.3+ of 2015-07-23 -- http://vsl.cis.udel.edu/civl

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

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

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