8 files changed, 20 insertions, 17 deletions
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 2df69b5d3..9b9b711ad 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -33,10 +33,11 @@
 #include "util/configuration.h"
 #include "util/exception.h"
 #include "util/language.h"
+#include "util/tls.h"
 
 ${include_all_option_headers}
 
-#line 40 "${template}"
+#line 41 "${template}"
 
 #include "util/output.h"
 #include "options/options_holder.h"
@@ -45,7 +46,7 @@ ${include_all_option_headers}
 
 ${option_handler_includes}
 
-#line 49 "${template}"
+#line 50 "${template}"
 
 using namespace CVC4;
 using namespace CVC4::options;
@@ -182,7 +183,7 @@ void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) {
 
 ${all_custom_handlers}
 
-#line 186 "${template}"
+#line 187 "${template}"
 
 #ifdef CVC4_DEBUG
 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
@@ -212,18 +213,18 @@ options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
 {
 }
 
-#line 216 "${template}"
+#line 217 "${template}"
 
 static const std::string mostCommonOptionsDescription = "\
 Most commonly-used CVC4 options:${common_documentation}";
 
-#line 221 "${template}"
+#line 222 "${template}"
 
 static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
 \n\
 Additional CVC4 options:${remaining_documentation}";
 
-#line 227 "${template}"
+#line 228 "${template}"
 
 static const std::string languageDescription = "\
 Languages currently supported as arguments to the -L / --lang option:\n\
@@ -287,7 +288,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options}
   { NULL, no_argument, NULL, '\0' }
 };/* cmdlineOptions */
 
-#line 291 "${template}"
+#line 292 "${template}"
 
 static void preemptGetopt(int& argc, char**& argv, const char* opt) {
   const size_t maxoptlen = 128;
@@ -320,10 +321,10 @@ namespace options {
 
 /** Set a given Options* as "current" just for a particular scope. */
 class OptionsGuard {
-  Options** d_field;
+  CVC4_THREADLOCAL_TYPE(Options*)* d_field;
   Options* d_old;
 public:
-  OptionsGuard(Options** field, Options* opts) :
+  OptionsGuard(CVC4_THREADLOCAL_TYPE(Options*)* field, Options* opts) :
     d_field(field),
     d_old(*field) {
     *field = opts;
@@ -414,7 +415,7 @@ int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
     switch(c) {
 ${all_modules_option_handlers}
 
-#line 418 "${template}"
+#line 419 "${template}"
 
     case ':':
       // This can be a long or short option, and the way to get at the
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index 3561e3c7b..e62baa2f6 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -37,7 +37,7 @@ class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> {
 public:
 
   RationalEnumerator(TypeNode type) throw(AssertionException) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<RationalEnumerator>(type),
     d_rat(0) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == REAL_TYPE);
@@ -80,7 +80,7 @@ class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
 public:
 
   IntegerEnumerator(TypeNode type) throw(AssertionException) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<IntegerEnumerator>(type),
     d_int(0) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == INTEGER_TYPE);
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index adea9a9e8..e613fc667 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -36,7 +36,7 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
 public:
 
   ArrayEnumerator(TypeNode type) throw(AssertionException) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<ArrayEnumerator>(type),
     d_index(TypeEnumerator(type.getArrayIndexType())),
     d_constituent(TypeEnumerator(type.getArrayConstituentType())) {
   }
diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h
index 36fb6d855..c83e79d75 100644
--- a/src/theory/booleans/type_enumerator.h
+++ b/src/theory/booleans/type_enumerator.h
@@ -35,7 +35,7 @@ class BooleanEnumerator : public TypeEnumeratorBase<BooleanEnumerator> {
 public:
 
   BooleanEnumerator(TypeNode type) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<BooleanEnumerator>(type),
     d_value(FALSE) {
     Assert(type.getKind() == kind::TYPE_CONSTANT &&
            type.getConst<TypeConstant>() == BOOLEAN_TYPE);
diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index 4893c2100..c94ec7322 100644
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -37,7 +37,7 @@ class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortE
 public:
 
   UninterpretedSortEnumerator(TypeNode type) throw(AssertionException) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<UninterpretedSortEnumerator>(type),
     d_count(0) {
     Assert(type.getKind() == kind::SORT_TYPE);
   }
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 01d431303..746e77a00 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -38,7 +38,7 @@ class BitVectorEnumerator : public TypeEnumeratorBase<BitVectorEnumerator> {
 public:
 
   BitVectorEnumerator(TypeNode type) throw(AssertionException) :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<BitVectorEnumerator>(type),
     d_size(type.getBitVectorSize()),
     d_bits(0) {
   }
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 76d49ecee..1776bf4ce 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -62,7 +62,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
 public:
 
   DatatypesEnumerator(TypeNode type) throw() :
-    TypeEnumeratorBase(type),
+    TypeEnumeratorBase<DatatypesEnumerator>(type),
     d_datatype(DatatypeType(type.toType()).getDatatype()),
     d_ctor(0),
     d_zeroCtor(0),
diff --git a/src/util/tls.h.in b/src/util/tls.h.in
index e77d256dc..df53cae36 100644
--- a/src/util/tls.h.in
+++ b/src/util/tls.h.in
@@ -33,10 +33,12 @@
 #if @CVC4_TLS_SUPPORTED@
 #  define CVC4_THREADLOCAL(__type...) @CVC4_TLS@ __type
 #  define CVC4_THREADLOCAL_PUBLIC(__type...) @CVC4_TLS@ CVC4_PUBLIC __type
+#  define CVC4_THREADLOCAL_TYPE(__type...) __type
 #else
 #  include <pthread.h>
 #  define CVC4_THREADLOCAL(__type...) ::CVC4::ThreadLocal< __type >
 #  define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC ::CVC4::ThreadLocal< __type >
+#  define CVC4_THREADLOCAL_TYPE(__type...) ::CVC4::ThreadLocal< __type >
 
 namespace CVC4 {