tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=2 -inputNP=2 -inputNX_BOUND=6
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 2)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 2
            NX_BOUND = 6

Starting search to compare diffusion_seq and ghost...Search complete.

STATS:
   statesSeen          :     4886
   statesMatched       :        0
   statesSaved         :       58
   transitionsExecuted :     4885
   transitionsStacked  :       29
   valuesSaved         :      226
   messagesSaved       :        0
   queries             :       29
   proverValidCalls    :       16
   memory              : 85000192
   time (s)            : 0.8

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=3 -inputNP=3 -inputNX_BOUND=9
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 3)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 3
            NX_BOUND = 9

Starting search to compare diffusion_seq and ghost...Search complete.

STATS:
   statesSeen          :    10537
   statesMatched       :        0
   statesSaved         :       83
   transitionsExecuted :    10536
   transitionsStacked  :       41
   valuesSaved         :      360
   messagesSaved       :        0
   queries             :       35
   proverValidCalls    :       20
   memory              : 85000192
   time (s)            : 1.23

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=4 -inputNP=4 -inputNX_BOUND=12
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 4)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 4
            NX_BOUND = 12

Starting search to compare diffusion_seq and ghost...Search complete.

STATS:
   statesSeen          :    18624
   statesMatched       :        0
   statesSaved         :      107
   transitionsExecuted :    18623
   transitionsStacked  :       53
   valuesSaved         :      525
   messagesSaved       :        0
   queries             :       41
   proverValidCalls    :       24
   memory              : 85000192
   time (s)            : 1.781

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=5 -inputNP=5 -inputNX_BOUND=15
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 5)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 5
            NX_BOUND = 15

Starting search to compare diffusion_seq and ghost...Search complete.

STATS:
   statesSeen          :    29363
   statesMatched       :        0
   statesSaved         :      131
   transitionsExecuted :    29362
   transitionsStacked  :       65
   valuesSaved         :      722
   messagesSaved       :        0
   queries             :       47
   proverValidCalls    :       28
   memory              : 85000192
   time (s)            : 2.322

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=6 -inputNP=6 -inputNX_BOUND=18
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 6)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 6
            NX_BOUND = 18

Starting search to compare diffusion_seq and ghost...Search complete.

STATS:
   statesSeen          :    42970
   statesMatched       :        0
   statesSaved         :      155
   transitionsExecuted :    42969
   transitionsStacked  :       77
   valuesSaved         :      951
   messagesSaved       :        0
   queries             :       53
   proverValidCalls    :       32
   memory              : 85000192
   time (s)            : 2.98

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=7 -inputNP=7 -inputNX_BOUND=21
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 7)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 7
            NX_BOUND = 21

Starting search to compare diffusion_seq and ghost...Search complete.

STATS:
   statesSeen          :    59661
   statesMatched       :        0
   statesSaved         :      179
   transitionsExecuted :    59660
   transitionsStacked  :       89
   valuesSaved         :     1212
   messagesSaved       :        0
   queries             :       59
   proverValidCalls    :       36
   memory              : 85000192
   time (s)            : 3.7

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=8 -inputNP=8 -inputNX_BOUND=24
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 8)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 8
            NX_BOUND = 24

Starting search to compare diffusion_seq and ghost...Search complete.

STATS:
   statesSeen          :    79652
   statesMatched       :        0
   statesSaved         :      203
   transitionsExecuted :    79651
   transitionsStacked  :      101
   valuesSaved         :     1505
   messagesSaved       :        0
   queries             :       65
   proverValidCalls    :       40
   memory              : 85000192
   time (s)            : 4.743

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=9 -inputNP=9 -inputNX_BOUND=27
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 9)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 9
            NX_BOUND = 27

Starting search to compare diffusion_seq and ghost...
    transitionsExecuted: 100000    statesSeen: 100000    statesSaved: 221
Search complete.

STATS:
   statesSeen          :   103159
   statesMatched       :        0
   statesSaved         :      227
   transitionsExecuted :   103158
   transitionsStacked  :      113
   valuesSaved         :     1830
   messagesSaved       :        0
   queries             :       71
   proverValidCalls    :       44
   memory              : 85000192
   time (s)            : 6.238

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=10 -inputNP=10 -inputNX_BOUND=30
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 10)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 10
            NX_BOUND = 30

Starting search to compare diffusion_seq and ghost...
    transitionsExecuted: 100000    statesSeen: 100000    statesSaved: 195
Search complete.

STATS:
   statesSeen          :   130398
   statesMatched       :        0
   statesSaved         :      251
   transitionsExecuted :   130397
   transitionsStacked  :      125
   valuesSaved         :     2187
   messagesSaved       :        0
   queries             :       77
   proverValidCalls    :       48
   memory              : 85000192
   time (s)            : 7.579

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=11 -inputNP=11 -inputNX_BOUND=33
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 11)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 11
            NX_BOUND = 33

Starting search to compare diffusion_seq and ghost...
    transitionsExecuted: 100000    statesSeen: 100000    statesSaved: 173
Search complete.

STATS:
   statesSeen          :   161585
   statesMatched       :        0
   statesSaved         :      275
   transitionsExecuted :   161584
   transitionsStacked  :      137
   valuesSaved         :     2576
   messagesSaved       :        0
   queries             :       83
   proverValidCalls    :       52
   memory              : 85000192
   time (s)            : 9.389

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=12 -inputNP=12 -inputNX_BOUND=36
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 12)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 12
            NX_BOUND = 36

Starting search to compare diffusion_seq and ghost...
    transitionsExecuted: 100000    statesSeen: 100000    statesSaved: 163
Search complete.

STATS:
   statesSeen          :   196936
   statesMatched       :        0
   statesSaved         :      299
   transitionsExecuted :   196935
   transitionsStacked  :      149
   valuesSaved         :     2997
   messagesSaved       :        0
   queries             :       89
   proverValidCalls    :       56
   memory              : 85000192
   time (s)            : 11.477

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=13 -inputNP=13 -inputNX_BOUND=39
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 13)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 13
            NX_BOUND = 39

Starting search to compare diffusion_seq and ghost...
    transitionsExecuted: 100000    statesSeen: 100000    statesSaved: 151
    transitionsExecuted: 200000    statesSeen: 200000    statesSaved: 269
Search complete.

STATS:
   statesSeen          :   236667
   statesMatched       :        0
   statesSaved         :      323
   transitionsExecuted :   236666
   transitionsStacked  :      161
   valuesSaved         :     3450
   messagesSaved       :        0
   queries             :       95
   proverValidCalls    :       60
   memory              : 85000192
   time (s)            : 15.017

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=14 -inputNP=14 -inputNX_BOUND=42
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 14)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 14
            NX_BOUND = 42

Starting search to compare diffusion_seq and ghost...
    transitionsExecuted: 100000    statesSeen: 100000    statesSaved: 143
    transitionsExecuted: 200000    statesSeen: 200000    statesSaved: 251
Search complete.

STATS:
   statesSeen          :   280994
   statesMatched       :        0
   statesSaved         :      347
   transitionsExecuted :   280993
   transitionsStacked  :      173
   valuesSaved         :     3935
   messagesSaved       :        0
   queries             :      101
   proverValidCalls    :       64
   memory              : 85000192
   time (s)            : 18.494

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=false -np2=15 -inputNP=15 -inputNX_BOUND=45
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2073M, 2010-10-27)                       |
+----------------------------------------------------------------------+
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : diffusion_seq.c
      implementation : ghost (numProcs = 15)
      implSourceFile : ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
        NSTEPS_BOUND = 2
                  NP = 15
            NX_BOUND = 45

Starting search to compare diffusion_seq and ghost...
    transitionsExecuted: 100000    statesSeen: 100000    statesSaved: 139
    transitionsExecuted: 200000    statesSeen: 200000    statesSaved: 229
    transitionsExecuted: 300000    statesSeen: 300000    statesSaved: 335
Search complete.

STATS:
   statesSeen          :   330133
   statesMatched       :        0
   statesSaved         :      371
   transitionsExecuted :   330132
   transitionsStacked  :      185
   valuesSaved         :     4452
   messagesSaved       :        0
   queries             :      107
   proverValidCalls    :       68
   memory              : 85000192
   time (s)            : 22.333

RESULT: The specified properties hold on all executions.

