summaryrefslogtreecommitdiff
path: root/src/util/hash.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-10-06 08:31:35 +0000
committerMorgan Deters <mdeters@gmail.com>2010-10-06 08:31:35 +0000
commitce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 (patch)
tree4ff6643e38469ceb84cd6791c5cbc295f625a735 /src/util/hash.h
parent4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (diff)
declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)
Diffstat (limited to 'src/util/hash.h')
-rw-r--r--src/util/hash.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/util/hash.h b/src/util/hash.h
index 2ce2d2941..cca60ce76 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -17,6 +17,8 @@
** \todo document this file
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__HASH_H
#define __CVC4__HASH_H
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback