summaryrefslogtreecommitdiffstats
path: root/src/aig/gia/giaAbsVta.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-07-07 14:33:54 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-07-07 14:33:54 -0700
commit44f04004fd02f3a8046b00168fd4432f0afe2331 (patch)
tree014b7ea40459d71ff66215dd2bca0afea8607c08 /src/aig/gia/giaAbsVta.c
parente22f5d1246c18dac711f2b6f6dc74d91ff3af3e5 (diff)
downloadabc-44f04004fd02f3a8046b00168fd4432f0afe2331.tar.gz
abc-44f04004fd02f3a8046b00168fd4432f0afe2331.tar.bz2
abc-44f04004fd02f3a8046b00168fd4432f0afe2331.zip
Adding memory report to print-outs produced by &vta and &gla.
Diffstat (limited to 'src/aig/gia/giaAbsVta.c')
-rw-r--r--src/aig/gia/giaAbsVta.c2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 00d239f3..6358f957 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1246,6 +1246,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
for ( k = 0; k < 7; k++ )
Abc_Print( 1, " " );
Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
+ Abc_Print( 1, "%5.1f Gb", sat_solver2_memory_proof( p->pSat ) / (1<<30) );
Abc_Print( 1, "\r" );
}
else
@@ -1267,6 +1268,7 @@ int Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCo
Abc_Print( 1, " " );
}
Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
+ Abc_Print( 1, "%5.1f Gb", sat_solver2_memory_proof( p->pSat ) / (1<<30) );
Abc_Print( 1, "\n" );
}
fflush( stdout );