tass verify -np=6 -deadlock=potential any_src-can-deadlock.c
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                       v1.2 (r1349, 2016-05-31)                       |
+----------------------------------------------------------------------+
               model : any_src-can-deadlock (numProcs = 6)
          sourceFile : any_src-can-deadlock.c
                mode : VERIFY
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1

Starting search to verify any_src-can-deadlock...
 ************ ERROR DETECTED ************
Execution error (kind: DEADLOCK, certainty: PROVEABLE)
Deadlock can occur at State 1238.
 with:
  Process 0 at location 4: libmpi.c 185.2--185.26: "send(_tmp, _dest, _tag);"
  Process 1 at location 4: libmpi.c 185.2--185.26: "send(_tmp, _dest, _tag);"
  Process 2 at location 10: libmpi.c 310.4--310.37: "send(tmp, 0, MPIX_BARRIER_ENTER);"
  Process 3 at location 10: libmpi.c 310.4--310.37: "send(tmp, 0, MPIX_BARRIER_ENTER);"
  Process 4 at location 10: libmpi.c 310.4--310.37: "send(tmp, 0, MPIX_BARRIER_ENTER);"
  Process 5 at location 10: libmpi.c 310.4--310.37: "send(tmp, 0, MPIX_BARRIER_ENTER);"

Writing trace to any_src-can-deadlock_0.trace...done.

Writing model any_src-can-deadlock.model...done.
Terminating search before completion.

STATS:
   statesSeen          :     76054
   statesMatched       :       260
   statesSaved         :       490
   transitionsExecuted :     76312
   transitionsStacked  :       365
   valuesSaved         :       446
   messagesSaved       :         7
   queries             :         3
   proverValidCalls    :         1
   memory              : 906493952
   time (s)            : 4.656

RESULT: Some properties MAY NOT hold: counterexample found.
NOTE: Search not complete.

tass verify -np=6 -deadlock=potential complex-deadlock.c
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                       v1.2 (r1349, 2016-05-31)                       |
+----------------------------------------------------------------------+
               model : complex-deadlock (numProcs = 6)
          sourceFile : complex-deadlock.c
                mode : VERIFY
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1

Starting search to verify complex-deadlock...
 ************ ERROR DETECTED ************
Execution error (kind: DEADLOCK, certainty: PROVEABLE)
Deadlock can occur at State 2.
 with:
  Process 0 at location 1: libmpi.c 249.4--249.39: "recv(_tmp, _source, _tag, thesize);"
  Process 1 at location 1: libmpi.c 249.4--249.39: "recv(_tmp, _source, _tag, thesize);"
  Process 2 at location 10: libmpi.c 310.4--310.37: "send(tmp, 0, MPIX_BARRIER_ENTER);"
  Process 3 at location 10: libmpi.c 310.4--310.37: "send(tmp, 0, MPIX_BARRIER_ENTER);"
  Process 4 at location 10: libmpi.c 310.4--310.37: "send(tmp, 0, MPIX_BARRIER_ENTER);"
  Process 5 at location 10: libmpi.c 310.4--310.37: "send(tmp, 0, MPIX_BARRIER_ENTER);"

Writing trace to complex-deadlock_0.trace...done.

Writing model complex-deadlock.model...done.
Terminating search before completion.

STATS:
   statesSeen          :       230
   statesMatched       :         0
   statesSaved         :         2
   transitionsExecuted :       229
   transitionsStacked  :         1
   valuesSaved         :        49
   messagesSaved       :         0
   queries             :         3
   proverValidCalls    :         1
   memory              : 514850816
   time (s)            : 0.102

RESULT: Some properties MAY NOT hold: counterexample found.
NOTE: Search not complete.

tass verify -np=6 -deadlock=potential sendrecv-deadlock.c
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                       v1.2 (r1349, 2016-05-31)                       |
+----------------------------------------------------------------------+
               model : sendrecv-deadlock (numProcs = 6)
          sourceFile : sendrecv-deadlock.c
                mode : VERIFY
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1

Starting search to verify sendrecv-deadlock...
 ************ ERROR DETECTED ************
Execution error (kind: DEADLOCK, certainty: PROVEABLE)
Deadlock can occur at State 2.
 with:
  Process 0 at location 1: libmpi.c 249.4--249.39: "recv(_tmp, _source, _tag, thesize);"
  Process 1 at location 4: libmpi.c 185.2--185.26: "send(_tmp, _dest, _tag);"
  Process 2 at location 4: libmpi.c 185.2--185.26: "send(_tmp, _dest, _tag);"
  Process 3 at location 10: libmpi.c 310.4--310.37: "send(tmp, 0, MPIX_BARRIER_ENTER);"
  Process 4 at location 10: libmpi.c 310.4--310.37: "send(tmp, 0, MPIX_BARRIER_ENTER);"
  Process 5 at location 10: libmpi.c 310.4--310.37: "send(tmp, 0, MPIX_BARRIER_ENTER);"

Writing trace to sendrecv-deadlock_0.trace...done.

Writing model sendrecv-deadlock.model...done.
Terminating search before completion.

STATS:
   statesSeen          :      1768
   statesMatched       :         0
   statesSaved         :         2
   transitionsExecuted :      1767
   transitionsStacked  :         1
   valuesSaved         :       560
   messagesSaved       :         0
   queries             :         3
   proverValidCalls    :         1
   memory              : 514850816
   time (s)            : 0.304

RESULT: Some properties MAY NOT hold: counterexample found.
NOTE: Search not complete.

