tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :      286
   messagesSaved       :        0
   queries             :       33
   proverValidCalls    :       16
   memory              : 85000192
   time (s)            : 0.925

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :      470
   messagesSaved       :        0
   queries             :       41
   proverValidCalls    :       20
   memory              : 85000192
   time (s)            : 1.457

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :      699
   messagesSaved       :        0
   queries             :       49
   proverValidCalls    :       24
   memory              : 85000192
   time (s)            : 2.22

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :      974
   messagesSaved       :        0
   queries             :       57
   proverValidCalls    :       28
   memory              : 85000192
   time (s)            : 2.922

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :     1295
   messagesSaved       :        0
   queries             :       65
   proverValidCalls    :       32
   memory              : 85000192
   time (s)            : 4.245

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :     1661
   messagesSaved       :        0
   queries             :       73
   proverValidCalls    :       36
   memory              : 85000192
   time (s)            : 5.926

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :     2072
   messagesSaved       :        0
   queries             :       81
   proverValidCalls    :       40
   memory              : 85000192
   time (s)            : 8.638

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :     2528
   messagesSaved       :        0
   queries             :       89
   proverValidCalls    :       44
   memory              : 85000192
   time (s)            : 11.647

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :     3029
   messagesSaved       :        0
   queries             :       97
   proverValidCalls    :       48
   memory              : 85000192
   time (s)            : 16.47

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :     3575
   messagesSaved       :        0
   queries             :      105
   proverValidCalls    :       52
   memory              : 85000192
   time (s)            : 23.062

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :      4166
   messagesSaved       :         0
   queries             :       113
   proverValidCalls    :        56
   memory              : 111538176
   time (s)            : 32.468

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :      4802
   messagesSaved       :         0
   queries             :       121
   proverValidCalls    :        60
   memory              : 110211072
   time (s)            : 43.809

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :      5483
   messagesSaved       :         0
   queries             :       129
   proverValidCalls    :        64
   memory              : 129957888
   time (s)            : 59.585

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=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 : true
        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         :      6209
   messagesSaved       :         0
   queries             :       137
   proverValidCalls    :        68
   memory              : 129957888
   time (s)            : 78.381

RESULT: The specified properties hold on all executions.

