diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4d8c15493..c11c272be 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -240,6 +240,9 @@ elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
 elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD")
   message(STATUS "Platform: FreeBSD")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_")
+elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "NetBSD")
+  message(STATUS "Platform: NetBSD")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NetBSD_")
 elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD")
   message(STATUS "Platform: OpenBSD")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_")
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index fecc207d8..99de61703 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -69,6 +69,7 @@ IS_WINDOWS=False
 IS_LINUX=False
 IS_OSX=False
 IS_FREEBSD=False
+IS_NETBSD=False
 IS_OPENBSD=False
 IS_CYGWIN=False
 IS_CYGWIN_MINGW=False
@@ -141,6 +142,9 @@ def is_linux():
 def is_freebsd():
     return IS_FREEBSD
 
+def is_netbsd():
+    return IS_NETBSD
+
 def is_openbsd():
     return IS_OPENBSD
 
@@ -604,6 +608,8 @@ elif os.name == 'posix':
         IS_LINUX=True
     elif os.uname()[0] == 'FreeBSD':
         IS_FREEBSD=True
+    elif os.uname()[0] == 'NetBSD':
+        IS_NETBSD=True
     elif os.uname()[0] == 'OpenBSD':
         IS_OPENBSD=True
     elif os.uname()[0][:6] == 'CYGWIN':
@@ -1245,7 +1251,7 @@ def get_so_ext():
     sysname = os.uname()[0]
     if sysname == 'Darwin':
         return 'dylib'
-    elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD':
+    elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'NetBSD' or sysname == 'OpenBSD':
         return 'so'
     elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
         return 'dll'
@@ -1795,6 +1801,8 @@ class JavaDLLComponent(Component):
                 t = t.replace('PLATFORM', 'linux')
             elif IS_FREEBSD:
                 t = t.replace('PLATFORM', 'freebsd')
+            elif IS_NETBSD:
+                t = t.replace('PLATFORM', 'netbsd')
             elif IS_OPENBSD:
                 t = t.replace('PLATFORM', 'openbsd')
             elif IS_CYGWIN:
@@ -2504,6 +2512,13 @@ def mk_config():
             LDFLAGS        = '%s -lrt' % LDFLAGS
             SLIBFLAGS      = '-shared'
             SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
+        elif sysname == 'NetBSD':
+            CXXFLAGS       = '%s -D_NETBSD_' % CXXFLAGS
+            OS_DEFINES     = '-D_NETBSD_'
+            SO_EXT         = '.so'
+            LDFLAGS        = '%s -lrt' % LDFLAGS
+            SLIBFLAGS      = '-shared'
+            SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
         elif sysname == 'OpenBSD':
             CXXFLAGS       = '%s -D_OPENBSD_' % CXXFLAGS
             OS_DEFINES     = '-D_OPENBSD_'
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index 1ecca8ffe..a2a0cc269 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -33,8 +33,8 @@ Revision History:
 #include<sys/time.h>
 #include<sys/errno.h>
 #include<pthread.h>
-#elif defined(_LINUX_) || defined(_FREEBSD_)
-// Linux
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NetBSD_)
+// Linux & FreeBSD & NetBSD
 #include<errno.h>
 #include<pthread.h>
 #include<sched.h>
@@ -66,8 +66,8 @@ struct scoped_timer::imp {
     pthread_mutex_t  m_mutex;
     pthread_cond_t   m_condition_var;
     struct timespec  m_end_time;
-#elif defined(_LINUX_) || defined(_FREEBSD_)
-    // Linux & FreeBSD
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
+    // Linux & FreeBSD & NetBSD
     pthread_t       m_thread_id;
     pthread_mutex_t m_mutex;
     pthread_cond_t  m_cond;
@@ -104,7 +104,7 @@ struct scoped_timer::imp {
 
         return st;
     }
-#elif defined(_LINUX_) || defined(_FREEBSD_)
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
     static void* thread_func(void *arg) {
         scoped_timer::imp *st = static_cast<scoped_timer::imp*>(arg);
 
@@ -175,8 +175,8 @@ struct scoped_timer::imp {
 
         if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0)
             throw default_exception("failed to start timer thread");
-#elif defined(_LINUX_) || defined(_FREEBSD_)
-        // Linux & FreeBSD
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
+        // Linux & FreeBSD & NetBSD
         m_ms = ms;
         m_initialized = false;
         m_signal_sent = false;
@@ -216,8 +216,8 @@ struct scoped_timer::imp {
             throw default_exception("failed to destroy pthread condition variable");
         if (pthread_attr_destroy(&m_attributes) != 0)
             throw default_exception("failed to destroy pthread attributes object");
-#elif defined(_LINUX_) || defined(_FREEBSD_)
-        // Linux & FreeBSD
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
+        // Linux & FreeBSD & NetBSD
         bool init = false;
 
         // spin until timer thread has been created
diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h
index 9ba707af0..83e03a2f7 100644
--- a/src/util/stopwatch.h
+++ b/src/util/stopwatch.h
@@ -134,6 +134,11 @@ public:
 
 #include<ctime>
 
+#ifndef CLOCK_PROCESS_CPUTIME_ID
+/* BSD */
+# define CLOCK_PROCESS_CPUTIME_ID CLOCK_MONOTONIC
+#endif
+
 class stopwatch {
     unsigned long long m_time; // elapsed time in ns
     bool               m_running;