diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 3deb6fc17..8b7d53897 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -27,6 +27,9 @@ Revision History:
 #include "util/trace.h"
 #include "util/max_cliques.h"
 #include "util/gparams.h"
+#ifdef _MSC_VER
+# include <xmmintrin.h>
+#endif
 
 // define to update glue during propagation
 #define UPDATE_GLUE
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index b6abb785f..5b1f336d1 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -56,7 +56,6 @@ z3_add_component(util
     symbol.cpp
     timeit.cpp
     timeout.cpp
-    timer.cpp
     trace.cpp
     util.cpp
     warning.cpp
diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h
index e8665054b..5fe10fb3b 100644
--- a/src/util/stopwatch.h
+++ b/src/util/stopwatch.h
@@ -25,14 +25,17 @@ Revision History:
 
 class stopwatch
 {
-    std::chrono::time_point<std::chrono::steady_clock> m_start;
-    std::chrono::steady_clock::duration m_elapsed;
+    typedef decltype(std::chrono::steady_clock::now()) clock_t;
+    typedef decltype(std::chrono::steady_clock::now() - std::chrono::steady_clock::now()) duration_t;
+
+    clock_t m_start;
+    duration_t m_elapsed;
 #if Z3DEBUG
     bool m_running = false;
 #endif
     
     // FIXME: just use auto with VS 2015+
-    static decltype(std::chrono::steady_clock::now()) get() {
+    static clock_t get() {
         return std::chrono::steady_clock::now();
     }
 
@@ -46,7 +49,7 @@ public:
     }
 
     void reset() {
-        m_elapsed = std::chrono::steady_clock::duration::zero();
+        m_elapsed = duration_t::zero();
     }
     
     void start() {