diff options
Diffstat (limited to 'test/monniaux/picosat-965/main.c')
-rw-r--r-- | test/monniaux/picosat-965/main.c | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/test/monniaux/picosat-965/main.c b/test/monniaux/picosat-965/main.c index 03fad79f..13d7b0e5 100644 --- a/test/monniaux/picosat-965/main.c +++ b/test/monniaux/picosat-965/main.c @@ -1,7 +1,25 @@ +#define VERIMAG_MEASUREMENTS +#ifdef VERIMAG_MEASUREMENTS +#include "../clock.h" +#endif + int picosat_main (int, char **); int main (int argc, char **argv) { - return picosat_main (argc, argv); + +#ifdef VERIMAG_MEASUREMENTS + clock_prepare(); + clock_start(); +#endif + + int ret= picosat_main (argc, argv); + +#ifdef VERIMAG_MEASUREMENTS + clock_stop(); + print_total_clock(); +#endif + + return ret; } |