From c96a6982a04e8fa5b2b8900f1a8b1dc02f108d2e Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Fri, 13 Sep 2013 20:42:49 -0700
Subject: [PATCH] Add <ctime> header for time() in pdeque/pvector tests

---
 src/tests/util/pdeque.cpp  | 1 +
 src/tests/util/pvector.cpp | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/tests/util/pdeque.cpp b/src/tests/util/pdeque.cpp
index 1e5021ae1..f9eeecec3 100644
--- a/src/tests/util/pdeque.cpp
+++ b/src/tests/util/pdeque.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <cstdlib>
 #include <deque>
 #include <vector>
+#include <ctime>
 #include "util/test.h"
 #include "util/pdeque.h"
 using namespace lean;
diff --git a/src/tests/util/pvector.cpp b/src/tests/util/pvector.cpp
index 55194a9e8..2e9d18f9b 100644
--- a/src/tests/util/pvector.cpp
+++ b/src/tests/util/pvector.cpp
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <cstdlib>
 #include <vector>
+#include <ctime>
 #include "util/test.h"
 #include "util/pvector.h"
 #include "util/timeit.h"