tass compare -buffer=1000 -deadlock=ignore -inputL=2 -inputM=2 -inputN=8 matmat-seq.c matmat-par.c -np2=2
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2093M, 2010-11-22)                       |
+----------------------------------------------------------------------+
       specification : matmat-seq (numProcs = 1)
      specSourceFile : matmat-seq.c
      implementation : matmat-par (numProcs = 2)
      implSourceFile : matmat-par.c
                mode : COMPARE
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : true
         bufferBound : 1000
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
                   L = 2
                   M = 2
                   N = 8

Starting search to compare matmat-seq and matmat-par...Search complete.

STATS:
   statesSeen          :     1386
   statesMatched       :        0
   statesSaved         :       13
   transitionsExecuted :     1385
   transitionsStacked  :        1
   valuesSaved         :      157
   messagesSaved       :        9
   queries             :        6
   proverValidCalls    :        2
   memory              : 85000192
   time (s)            : 0.331

RESULT: The specified properties hold on all executions.

tass compare -buffer=1000 -deadlock=ignore -inputL=2 -inputM=2 -inputN=8 matmat-seq.c matmat-par.c -np2=3
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2093M, 2010-11-22)                       |
+----------------------------------------------------------------------+
       specification : matmat-seq (numProcs = 1)
      specSourceFile : matmat-seq.c
      implementation : matmat-par (numProcs = 3)
      implSourceFile : matmat-par.c
                mode : COMPARE
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : true
         bufferBound : 1000
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
                   L = 2
                   M = 2
                   N = 8

Starting search to compare matmat-seq and matmat-par...Search complete.

STATS:
   statesSeen          :    13003
   statesMatched       :       63
   statesSaved         :      392
   transitionsExecuted :    13042
   transitionsStacked  :      127
   valuesSaved         :      245
   messagesSaved       :       29
   queries             :        6
   proverValidCalls    :        2
   memory              : 85000192
   time (s)            : 1.359

RESULT: The specified properties hold on all executions.

tass compare -buffer=1000 -deadlock=ignore -inputL=2 -inputM=2 -inputN=8 matmat-seq.c matmat-par.c -np2=4
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2093M, 2010-11-22)                       |
+----------------------------------------------------------------------+
       specification : matmat-seq (numProcs = 1)
      specSourceFile : matmat-seq.c
      implementation : matmat-par (numProcs = 4)
      implSourceFile : matmat-par.c
                mode : COMPARE
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : true
         bufferBound : 1000
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
                   L = 2
                   M = 2
                   N = 8

Starting search to compare matmat-seq and matmat-par...Search complete.

STATS:
   statesSeen          :    89526
   statesMatched       :      629
   statesSaved         :     2242
   transitionsExecuted :    89966
   transitionsStacked  :     1039
   valuesSaved         :      323
   messagesSaved       :       38
   queries             :        6
   proverValidCalls    :        2
   memory              : 85000192
   time (s)            : 3.255

RESULT: The specified properties hold on all executions.

tass compare -buffer=1000 -deadlock=ignore -inputL=2 -inputM=2 -inputN=8 matmat-seq.c matmat-par.c -np2=5
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2093M, 2010-11-22)                       |
+----------------------------------------------------------------------+
       specification : matmat-seq (numProcs = 1)
      specSourceFile : matmat-seq.c
      implementation : matmat-par (numProcs = 5)
      implSourceFile : matmat-par.c
                mode : COMPARE
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : true
         bufferBound : 1000
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
                   L = 2
                   M = 2
                   N = 8

Starting search to compare matmat-seq and matmat-par...
    transitionsExecuted: 100000    statesSeen: 99230    statesSaved: 1968
    transitionsExecuted: 200000    statesSeen: 198424    statesSaved: 3927
    transitionsExecuted: 300000    statesSeen: 297617    statesSaved: 5904
Search complete.

STATS:
   statesSeen          :   376179
   statesMatched       :     3599
   statesSaved         :     7460
   transitionsExecuted :   379234
   transitionsStacked  :     6069
   valuesSaved         :      407
   messagesSaved       :       43
   queries             :        6
   proverValidCalls    :        2
   memory              : 85000192
   time (s)            : 8.567

RESULT: The specified properties hold on all executions.

tass compare -buffer=1000 -deadlock=ignore -inputL=2 -inputM=2 -inputN=8 matmat-seq.c matmat-par.c -np2=6
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2093M, 2010-11-22)                       |
+----------------------------------------------------------------------+
       specification : matmat-seq (numProcs = 1)
      specSourceFile : matmat-seq.c
      implementation : matmat-par (numProcs = 6)
      implSourceFile : matmat-par.c
                mode : COMPARE
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : true
         bufferBound : 1000
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
                   L = 2
                   M = 2
                   N = 8

Starting search to compare matmat-seq and matmat-par...
    transitionsExecuted: 100000    statesSeen: 98810    statesSaved: 1523
    transitionsExecuted: 200000    statesSeen: 197610    statesSaved: 3038
    transitionsExecuted: 300000    statesSeen: 296404    statesSaved: 4547
    transitionsExecuted: 400000    statesSeen: 395195    statesSaved: 6061
    transitionsExecuted: 500000    statesSeen: 493990    statesSaved: 7571
    transitionsExecuted: 600000    statesSeen: 592774    statesSaved: 9081
    transitionsExecuted: 700000    statesSeen: 691568    statesSaved: 10593
Search complete.

STATS:
   statesSeen          :   738244
   statesMatched       :     9549
   statesSaved         :    11294
   transitionsExecuted :   747268
   transitionsStacked  :    15481
   valuesSaved         :      469
   messagesSaved       :       44
   queries             :        6
   proverValidCalls    :        2
   memory              : 85000192
   time (s)            : 13.275

RESULT: The specified properties hold on all executions.

tass compare -buffer=1000 -deadlock=ignore -inputL=2 -inputM=2 -inputN=8 matmat-seq.c matmat-par.c -np2=7
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2093M, 2010-11-22)                       |
+----------------------------------------------------------------------+
       specification : matmat-seq (numProcs = 1)
      specSourceFile : matmat-seq.c
      implementation : matmat-par (numProcs = 7)
      implSourceFile : matmat-par.c
                mode : COMPARE
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : true
         bufferBound : 1000
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
                   L = 2
                   M = 2
                   N = 8

Starting search to compare matmat-seq and matmat-par...
    transitionsExecuted: 100000    statesSeen: 98514    statesSaved: 1219
    transitionsExecuted: 200000    statesSeen: 196992    statesSaved: 2406
    transitionsExecuted: 300000    statesSeen: 295469    statesSaved: 3592
    transitionsExecuted: 400000    statesSeen: 393934    statesSaved: 4767
    transitionsExecuted: 500000    statesSeen: 492395    statesSaved: 5937
    transitionsExecuted: 600000    statesSeen: 590880    statesSaved: 7135
Search complete.

STATS:
   statesSeen          :   683811
   statesMatched       :    10799
   statesSaved         :     8224
   transitionsExecuted :   694394
   transitionsStacked  :    16459
   valuesSaved         :      495
   messagesSaved       :       41
   queries             :        6
   proverValidCalls    :        2
   memory              : 85000192
   time (s)            : 11.107

RESULT: The specified properties hold on all executions.

tass compare -buffer=1000 -deadlock=ignore -inputL=2 -inputM=2 -inputN=8 matmat-seq.c matmat-par.c -np2=8
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2093M, 2010-11-22)                       |
+----------------------------------------------------------------------+
       specification : matmat-seq (numProcs = 1)
      specSourceFile : matmat-seq.c
      implementation : matmat-par (numProcs = 8)
      implSourceFile : matmat-par.c
                mode : COMPARE
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : true
         bufferBound : 1000
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
                   L = 2
                   M = 2
                   N = 8

Starting search to compare matmat-seq and matmat-par...
    transitionsExecuted: 100000    statesSeen: 98289    statesSaved: 990
    transitionsExecuted: 200000    statesSeen: 196552    statesSaved: 1959
    transitionsExecuted: 300000    statesSeen: 294811    statesSaved: 2924
Search complete.

STATS:
   statesSeen          :   356408
   statesMatched       :     6369
   statesSaved         :     3490
   transitionsExecuted :   362728
   transitionsStacked  :     9171
   valuesSaved         :      493
   messagesSaved       :       34
   queries             :        6
   proverValidCalls    :        2
   memory              : 85000192
   time (s)            : 6.633

RESULT: The specified properties hold on all executions.

tass compare -buffer=1000 -deadlock=ignore -inputL=2 -inputM=2 -inputN=8 matmat-seq.c matmat-par.c -np2=9
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|                     http://vsl.cis.udel.edu/tass                     |
|                      v1.1 (r2093M, 2010-11-22)                       |
+----------------------------------------------------------------------+
       specification : matmat-seq (numProcs = 1)
      specSourceFile : matmat-seq.c
      implementation : matmat-par (numProcs = 9)
      implSourceFile : matmat-par.c
                mode : COMPARE
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : true
         bufferBound : 1000
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : ./TASSREP
            frontend : ANTLR
          errorBound : 1
                   L = 2
                   M = 2
                   N = 8

Starting search to compare matmat-seq and matmat-par...
    transitionsExecuted: 100000    statesSeen: 98202    statesSaved: 900
Search complete.

STATS:
   statesSeen          :   133595
   statesMatched       :     2575
   statesSaved         :     1108
   transitionsExecuted :   136162
   transitionsStacked  :     3537
   valuesSaved         :      460
   messagesSaved       :       23
   queries             :        6
   proverValidCalls    :        2
   memory              : 85000192
   time (s)            : 3.481

RESULT: The specified properties hold on all executions.

