Other improvements to &vta and &gla.

2 files changed, 21 insertions, 15 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index f6ada0c8..cdfc7712 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -1925,14 +1925,17 @@ finish:
         p->pPars->iFrame = pCex->iFrame - 1;
     }
     Abc_PrintTime( 1, "Time", clock() - clk );
-    p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
-    ABC_PRTP( "Runtime: Initializing", p->timeInit,   clock() - clk );
-    ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  clock() - clk );
-    ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    clock() - clk );
-    ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    clock() - clk );
-    ABC_PRTP( "Runtime: Other       ", p->timeOther,  clock() - clk );
-    ABC_PRTP( "Runtime: TOTAL       ", clock() - clk, clock() - clk );
-    Gla_ManReportMemory( p );
+    if ( p->pPars->fVerbose )
+    {
+        p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
+        ABC_PRTP( "Runtime: Initializing", p->timeInit,   clock() - clk );
+        ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  clock() - clk );
+        ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    clock() - clk );
+        ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    clock() - clk );
+        ABC_PRTP( "Runtime: Other       ", p->timeOther,  clock() - clk );
+        ABC_PRTP( "Runtime: TOTAL       ", clock() - clk, clock() - clk );
+        Gla_ManReportMemory( p );
+    }
     Gla_ManStop( p );
     fflush( stdout );
     return RetValue;
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 1a442a79..e762c112 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1816,13 +1816,16 @@ finish:
     }
     Abc_PrintTime( 1, "Time", clock() - clk );
 
-    p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
-    ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  clock() - clk );
-    ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    clock() - clk );
-    ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    clock() - clk );
-    ABC_PRTP( "Runtime: Other       ", p->timeOther,  clock() - clk );
-    ABC_PRTP( "Runtime: TOTAL       ", clock() - clk, clock() - clk );
-    Gia_VtaPrintMemory( p );
+    if ( p->pPars->fVerbose )
+    {
+        p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
+        ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  clock() - clk );
+        ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    clock() - clk );
+        ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    clock() - clk );
+        ABC_PRTP( "Runtime: Other       ", p->timeOther,  clock() - clk );
+        ABC_PRTP( "Runtime: TOTAL       ", clock() - clk, clock() - clk );
+        Gia_VtaPrintMemory( p );
+    }
 
     Vga_ManStop( p );
     fflush( stdout );