summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2018-07-03 09:27:59 -0700
committerGitHub <noreply@github.com>2018-07-03 09:27:59 -0700
commit45a5d525d26dba9ed3f12d888c8b9fb844c8a8ec (patch)
treebeea5460c4b171e04da50e4d4e9fe16446dd2772 /src/util
parent55725be5569e27755538f2032cbe7bcb9353f310 (diff)
New C++ API: Implementation of Term. (#2131)
Diffstat (limited to 'src/util')
-rw-r--r--src/util/utility.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/util/utility.h b/src/util/utility.h
index bfe8e66c9..a9a9a29c3 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -19,6 +19,7 @@
#ifndef __CVC4__UTILITY_H
#define __CVC4__UTILITY_H
+#include <algorithm>
#include <utility>
#include <functional>
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback