File tree 2 files changed +4
-4
lines changed
2 files changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -67,9 +67,9 @@ static inline int memReadPeak(void)
67
67
}
68
68
69
69
double Minisat::memUsed () { return (double )memReadStat (0 ) * (double )getpagesize () / (1024 *1024 ); }
70
- double Minisat::memUsedPeak () {
71
- double peak = memReadPeak () / 1024 ;
72
- return peak == 0 ? memUsed () : peak; }
70
+ double Minisat::memUsedPeak (bool strictlyPeak ) {
71
+ double peak = memReadPeak () / ( double ) 1024 ;
72
+ return peak == 0 && !strictlyPeak ? memUsed () : peak; }
73
73
74
74
#elif defined(__FreeBSD__) || defined(__FreeBSD_kernel__) || defined(__gnu_hurd__)
75
75
Original file line number Diff line number Diff line change @@ -34,7 +34,7 @@ namespace Minisat {
34
34
static inline double cpuTime (void ); // CPU-time in seconds.
35
35
36
36
extern double memUsed (); // Memory in mega bytes (returns 0 for unsupported architectures).
37
- extern double memUsedPeak (); // Peak-memory in mega bytes (returns 0 for unsupported architectures).
37
+ extern double memUsedPeak (bool strictlyPeak = false ); // Peak-memory in mega bytes (returns 0 for unsupported architectures).
38
38
39
39
extern void setX86FPUPrecision (); // Make sure double's are represented with the same precision
40
40
// in memory and registers.
You can’t perform that action at this time.
0 commit comments