Prepared &gla to try abstracting and proving concurrently.

src/aig/gia/giaAbsGla2.c

@@ -1799,7 +1799,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             }
             // if abstraction grew more than a certain percentage, force a restart
             if ( pPars->nRatioMax == 0 )
-                break;
+                continue;
             if ( c > 0 && (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
             {
                 if ( p->pPars->fVerbose )

src/aig/gia/giaAbsOut.c

@@ -378,7 +378,7 @@ int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFra
     Gia_Man_t * pAbs, * pNew;
     Vec_Int_t * vFlops, * vInit;
     Vec_Int_t * vCopy;
-    clock_t clk = clock();
+//    clock_t clk = clock();
     int RetValue;
     ABC_FREE( p->pCexSeq );
     if ( p->vGateClasses == NULL )

src/aig/gia/giaAbsPth.c

@@ -21,9 +21,13 @@
 #include "aig/ioa/ioa.h"
 #include "proof/pdr/pdr.h"
 
-// comment this out to disable pthreads
+// uncomment this line to enable pthreads
 //#define ABC_USE_PTHREADS
 
+// to compile on Linux, modify Makefile as follows:
+// add -pthread to OPTFLAGS
+// add -lpthread to LIBS
+
 #ifdef ABC_USE_PTHREADS
 
 #ifdef WIN32