tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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          :     3496
   statesMatched       :        0
   statesSaved         :       58
   transitionsExecuted :     3495
   transitionsStacked  :       29
   valuesSaved         :      289
   messagesSaved       :        0
   queries             :       39
   proverValidCalls    :       17
   memory              : 85000192
   time (s)            : 0.827

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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          :     7492
   statesMatched       :        0
   statesSaved         :       83
   transitionsExecuted :     7491
   transitionsStacked  :       41
   valuesSaved         :      476
   messagesSaved       :        0
   queries             :       49
   proverValidCalls    :       21
   memory              : 85000192
   time (s)            : 1.323

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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          :    13188
   statesMatched       :        0
   statesSaved         :      107
   transitionsExecuted :    13187
   transitionsStacked  :       53
   valuesSaved         :      709
   messagesSaved       :        0
   queries             :       59
   proverValidCalls    :       25
   memory              : 85000192
   time (s)            : 1.856

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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          :    20728
   statesMatched       :        0
   statesSaved         :      131
   transitionsExecuted :    20727
   transitionsStacked  :       65
   valuesSaved         :      989
   messagesSaved       :        0
   queries             :       69
   proverValidCalls    :       29
   memory              : 85000192
   time (s)            : 2.417

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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          :    30256
   statesMatched       :        0
   statesSaved         :      155
   transitionsExecuted :    30255
   transitionsStacked  :       77
   valuesSaved         :     1316
   messagesSaved       :        0
   queries             :       79
   proverValidCalls    :       33
   memory              : 85000192
   time (s)            : 3.421

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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          :    41916
   statesMatched       :        0
   statesSaved         :      179
   transitionsExecuted :    41915
   transitionsStacked  :       89
   valuesSaved         :     1689
   messagesSaved       :        0
   queries             :       89
   proverValidCalls    :       37
   memory              : 85000192
   time (s)            : 4.821

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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          :    55852
   statesMatched       :        0
   statesSaved         :      203
   transitionsExecuted :    55851
   transitionsStacked  :      101
   valuesSaved         :     2108
   messagesSaved       :        0
   queries             :       99
   proverValidCalls    :       41
   memory              : 85000192
   time (s)            : 6.085

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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...Search complete.

STATS:
   statesSeen          :    72208
   statesMatched       :        0
   statesSaved         :      227
   transitionsExecuted :    72207
   transitionsStacked  :      113
   valuesSaved         :     2573
   messagesSaved       :        0
   queries             :      109
   proverValidCalls    :       45
   memory              : 85000192
   time (s)            : 8.328

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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...Search complete.

STATS:
   statesSeen          :    91128
   statesMatched       :        0
   statesSaved         :      251
   transitionsExecuted :    91127
   transitionsStacked  :      125
   valuesSaved         :     3084
   messagesSaved       :        0
   queries             :      119
   proverValidCalls    :       49
   memory              : 85000192
   time (s)            : 11.08

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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: 243
Search complete.

STATS:
   statesSeen          :   112756
   statesMatched       :        0
   statesSaved         :      275
   transitionsExecuted :   112755
   transitionsStacked  :      137
   valuesSaved         :     3641
   messagesSaved       :        0
   queries             :      129
   proverValidCalls    :       53
   memory              : 85000192
   time (s)            : 15.302

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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: 217
Search complete.

STATS:
   statesSeen          :    137236
   statesMatched       :         0
   statesSaved         :       299
   transitionsExecuted :    137235
   transitionsStacked  :       149
   valuesSaved         :      4244
   messagesSaved       :         0
   queries             :       139
   proverValidCalls    :        57
   memory              : 111603712
   time (s)            : 19.489

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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: 201
Search complete.

STATS:
   statesSeen          :    164712
   statesMatched       :         0
   statesSaved         :       323
   transitionsExecuted :    164711
   transitionsStacked  :       161
   valuesSaved         :      4893
   messagesSaved       :         0
   queries             :       149
   proverValidCalls    :        61
   memory              : 107814912
   time (s)            : 26.559

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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: 189
Search complete.

STATS:
   statesSeen          :    195328
   statesMatched       :         0
   statesSaved         :       347
   transitionsExecuted :    195327
   transitionsStacked  :       173
   valuesSaved         :      5588
   messagesSaved       :         0
   queries             :       159
   proverValidCalls    :        65
   memory              : 129957888
   time (s)            : 34.428

RESULT: The specified properties hold on all executions.

tass compare diffusion_seq.c ghost.c -inputNSTEPS_BOUND=2 -deadlock=potential -ca=true -cqmin=true -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: 175
    transitionsExecuted: 200000    statesSeen: 200000    statesSaved: 319
Search complete.

STATS:
   statesSeen          :    229228
   statesMatched       :         0
   statesSaved         :       371
   transitionsExecuted :    229227
   transitionsStacked  :       185
   valuesSaved         :      6329
   messagesSaved       :         0
   queries             :       169
   proverValidCalls    :        69
   memory              : 129957888
   time (s)            : 45.274

RESULT: The specified properties hold on all executions.

