merged master into branch

75 files changed, 1102 insertions, 565 deletions

diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index a085161bc..9a14caec5 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -752,7 +752,7 @@ public:
                      table_value_type table_value_type;
     typedef attr::AttributeTraits<table_value_type, context_dep> traits;
     uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
-    Assert(traits::cleanup.size() == id);// sanity check
+    //Assert(traits::cleanup.size() == id);// sanity check
     traits::cleanup.push_back(attr::getCleanupStrategy<value_t,
                                                        CleanupStrategy>::fn);
     return id;
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index b9cae9431..09018cbfd 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -43,7 +43,7 @@ class SmtEngine;
 class NodeManager;
 class Options;
 class IntStat;
-class ExprManagerMapCollection;
+struct ExprManagerMapCollection;
 class StatisticsRegistry;
 
 namespace expr {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 442d29ac9..b353ec5dc 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -67,7 +67,7 @@ namespace prop {
   class TheoryProxy;
 }/* CVC4::prop namespace */
 
-class ExprManagerMapCollection;
+struct ExprManagerMapCollection;
 
 struct ExprHashFunction;
 
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 47504b0e4..0cab4e628 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -27,7 +27,7 @@
 namespace CVC4 {
 namespace kind {
 
-enum Kind_t {
+enum CVC4_PUBLIC Kind_t {
   UNDEFINED_KIND = -1, /**< undefined */
   NULL_EXPR, /**< Null kind */
 ${kind_decls}
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index cc52b11b9..4e95c0fe2 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -204,111 +204,48 @@ bool Type::isBoolean() const {
   return d_typeNode->isBoolean();
 }
 
-/** Cast to a Boolean type */
-Type::operator BooleanType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isBoolean(), this);
-  return BooleanType(*this);
-}
-
 /** Is this the integer type? */
 bool Type::isInteger() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isInteger();
 }
 
-/** Cast to a integer type */
-Type::operator IntegerType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isInteger(), this);
-  return IntegerType(*this);
-}
-
 /** Is this the real type? */
 bool Type::isReal() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isReal();
 }
 
-/** Cast to a real type */
-Type::operator RealType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isReal(), this);
-  return RealType(*this);
-}
-
 /** Is this the string type? */
 bool Type::isString() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isString();
 }
 
-/** Cast to a string type */
-Type::operator StringType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isString(), this);
-  return StringType(*this);
-}
-
 /** Is this the bit-vector type? */
 bool Type::isBitVector() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isBitVector();
 }
 
-/** Cast to a bit-vector type */
-Type::operator BitVectorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isBitVector(), this);
-  return BitVectorType(*this);
-}
-
-/** Cast to a Constructor type */
-Type::operator DatatypeType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isDatatype(), this);
-  return DatatypeType(*this);
-}
-
 /** Is this a datatype type? */
 bool Type::isDatatype() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype();
 }
 
-/** Cast to a Constructor type */
-Type::operator ConstructorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isConstructor(), this);
-  return ConstructorType(*this);
-}
-
 /** Is this the Constructor type? */
 bool Type::isConstructor() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isConstructor();
 }
 
-/** Cast to a Selector type */
-Type::operator SelectorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSelector(), this);
-  return SelectorType(*this);
-}
-
 /** Is this the Selector type? */
 bool Type::isSelector() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSelector();
 }
 
-/** Cast to a Tester type */
-Type::operator TesterType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isTester(), this);
-  return TesterType(*this);
-}
-
 /** Is this the Tester type? */
 bool Type::isTester() const {
   NodeManagerScope nms(d_nodeManager);
@@ -330,64 +267,30 @@ bool Type::isPredicate() const {
   return d_typeNode->isPredicate();
 }
 
-/** Cast to a function type */
-Type::operator FunctionType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isFunction(), this);
-  return FunctionType(*this);
-}
-
 /** Is this a tuple type? */
 bool Type::isTuple() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isTuple();
 }
 
-/** Cast to a tuple type */
-Type::operator TupleType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isTuple(), this);
-  return TupleType(*this);
-}
-
 /** Is this a record type? */
 bool Type::isRecord() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isRecord();
 }
 
-/** Cast to a record type */
-Type::operator RecordType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isRecord(), this);
-  return RecordType(*this);
-}
-
 /** Is this a symbolic expression type? */
 bool Type::isSExpr() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSExpr();
 }
 
-/** Cast to a symbolic expression type */
-Type::operator SExprType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSExpr(), this);
-  return SExprType(*this);
-}
-
 /** Is this an array type? */
 bool Type::isArray() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isArray();
 }
 
-/** Cast to an array type */
-Type::operator ArrayType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  return ArrayType(*this);
-}
-
 /** Is this a sort kind */
 bool Type::isSort() const {
   NodeManagerScope nms(d_nodeManager);
@@ -395,25 +298,11 @@ bool Type::isSort() const {
 }
 
 /** Cast to a sort type */
-Type::operator SortType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSort(), this);
-  return SortType(*this);
-}
-
-/** Is this a sort constructor kind */
 bool Type::isSortConstructor() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSortConstructor();
 }
 
-/** Cast to a sort constructor type */
-Type::operator SortConstructorType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSortConstructor(), this);
-  return SortConstructorType(*this);
-}
-
 /** Is this a predicate subtype */
 /* - not in release 1.0
 bool Type::isPredicateSubtype() const {
@@ -422,28 +311,12 @@ bool Type::isPredicateSubtype() const {
 }
 */
 
-/** Cast to a predicate subtype */
-/* - not in release 1.0
-Type::operator PredicateSubtype() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isPredicateSubtype(), this);
-  return PredicateSubtype(*this);
-}
-*/
-
 /** Is this an integer subrange */
 bool Type::isSubrange() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isSubrange();
 }
 
-/** Cast to a predicate subtype */
-Type::operator SubrangeType() const throw(IllegalArgumentException) {
-  NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isSubrange(), this);
-  return SubrangeType(*this);
-}
-
 vector<Type> FunctionType::getArgTypes() const {
   NodeManagerScope nms(d_nodeManager);
   vector<Type> args;
diff --git a/src/expr/type.h b/src/expr/type.h
index 4223d71ab..ce6291cd8 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -30,15 +30,15 @@
 namespace CVC4 {
 
 class NodeManager;
-class ExprManager;
-class Expr;
+class CVC4_PUBLIC ExprManager;
+class CVC4_PUBLIC Expr;
 class TypeNode;
-class ExprManagerMapCollection;
+struct CVC4_PUBLIC ExprManagerMapCollection;
 
-class SmtEngine;
+class CVC4_PUBLIC SmtEngine;
 
-class Datatype;
-class Record;
+class CVC4_PUBLIC Datatype;
+class CVC4_PUBLIC Record;
 
 template <bool ref_count>
 class NodeTemplate;
@@ -240,60 +240,30 @@ public:
   bool isBoolean() const;
 
   /**
-   * Cast this type to a Boolean type
-   * @return the BooleanType
-   */
-  operator BooleanType() const throw(IllegalArgumentException);
-
-  /**
    * Is this the integer type?
    * @return true if the type is a integer type
    */
   bool isInteger() const;
 
   /**
-   * Cast this type to a integer type
-   * @return the IntegerType
-   */
-  operator IntegerType() const throw(IllegalArgumentException);
-
-  /**
    * Is this the real type?
    * @return true if the type is a real type
    */
   bool isReal() const;
 
   /**
-   * Cast this type to a real type
-   * @return the RealType
-   */
-  operator RealType() const throw(IllegalArgumentException);
-
-  /**
    * Is this the string type?
    * @return true if the type is the string type
    */
   bool isString() const;
 
   /**
-   * Cast this type to a string type
-   * @return the StringType
-   */
-  operator StringType() const throw(IllegalArgumentException);
-
-  /**
    * Is this the bit-vector type?
    * @return true if the type is a bit-vector type
    */
   bool isBitVector() const;
 
   /**
-   * Cast this type to a bit-vector type
-   * @return the BitVectorType
-   */
-  operator BitVectorType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a function type?
    * @return true if the type is a function type
    */
@@ -307,132 +277,66 @@ public:
   bool isPredicate() const;
 
   /**
-   * Cast this type to a function type
-   * @return the FunctionType
-   */
-  operator FunctionType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a tuple type?
    * @return true if the type is a tuple type
    */
   bool isTuple() const;
 
   /**
-   * Cast this type to a tuple type
-   * @return the TupleType
-   */
-  operator TupleType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a record type?
    * @return true if the type is a record type
    */
   bool isRecord() const;
 
   /**
-   * Cast this type to a record type
-   * @return the RecordType
-   */
-  operator RecordType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a symbolic expression type?
    * @return true if the type is a symbolic expression type
    */
   bool isSExpr() const;
 
   /**
-   * Cast this type to a symbolic expression type
-   * @return the SExprType
-   */
-  operator SExprType() const throw(IllegalArgumentException);
-
-  /**
    * Is this an array type?
    * @return true if the type is a array type
    */
   bool isArray() const;
 
   /**
-   * Cast this type to an array type
-   * @return the ArrayType
-   */
-  operator ArrayType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a datatype type?
    * @return true if the type is a datatype type
    */
   bool isDatatype() const;
 
   /**
-   * Cast this type to a datatype type
-   * @return the DatatypeType
-   */
-  operator DatatypeType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a constructor type?
    * @return true if the type is a constructor type
    */
   bool isConstructor() const;
 
   /**
-   * Cast this type to a constructor type
-   * @return the ConstructorType
-   */
-  operator ConstructorType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a selector type?
    * @return true if the type is a selector type
    */
   bool isSelector() const;
 
   /**
-   * Cast this type to a selector type
-   * @return the SelectorType
-   */
-  operator SelectorType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a tester type?
    * @return true if the type is a tester type
    */
   bool isTester() const;
 
   /**
-   * Cast this type to a tester type
-   * @return the TesterType
-   */
-  operator TesterType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a sort kind?
    * @return true if this is a sort kind
    */
   bool isSort() const;
 
   /**
-   * Cast this type to a sort type
-   * @return the sort type
-   */
-  operator SortType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a sort constructor kind?
    * @return true if this is a sort constructor kind
    */
   bool isSortConstructor() const;
 
   /**
-   * Cast this type to a sort constructor type
-   * @return the sort constructor type
-   */
-  operator SortConstructorType() const throw(IllegalArgumentException);
-
-  /**
    * Is this a predicate subtype?
    * @return true if this is a predicate subtype
    */
@@ -440,25 +344,12 @@ public:
   //bool isPredicateSubtype() const;
 
   /**
-   * Cast this type to a predicate subtype
-   * @return the predicate subtype
-   */
-  // not in release 1.0
-  //operator PredicateSubtype() const throw(IllegalArgumentException);
-
-  /**
    * Is this an integer subrange type?
    * @return true if this is an integer subrange type
    */
   bool isSubrange() const;
 
   /**
-   * Cast this type to an integer subrange type
-   * @return the integer subrange type
-   */
-  operator SubrangeType() const throw(IllegalArgumentException);
-
-  /**
    * Outputs a string representation of this type to the stream.
    * @param out the stream to output to
    */
diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h
index 6c546a147..9993e5f18 100644
--- a/src/include/cvc4_public.h
+++ b/src/include/cvc4_public.h
@@ -22,19 +22,7 @@
 #include <stdint.h>
 
 #if defined _WIN32 || defined __CYGWIN__
-#  ifdef BUILDING_DLL
-#    ifdef __GNUC__
-#      define CVC4_PUBLIC __attribute__((__dllexport__))
-#    else /* ! __GNUC__ */
-#      define CVC4_PUBLIC __declspec(dllexport)
-#    endif /* __GNUC__ */
-#  else /* BUILDING_DLL */
-#    ifdef __GNUC__
-#      define CVC4_PUBLIC __attribute__((__dllimport__))
-#    else /* ! __GNUC__ */
-#      define CVC4_PUBLIC __declspec(dllimport)
-#    endif /* __GNUC__ */
-#  endif /* BUILDING_DLL */
+#  define CVC4_PUBLIC
 #else /* !( defined _WIN32 || defined __CYGWIN__ ) */
 #  if __GNUC__ >= 4
 #    define CVC4_PUBLIC __attribute__ ((__visibility__("default")))
diff --git a/src/lib/Makefile.am b/src/lib/Makefile.am
index a6ea59e95..61f9e2d70 100644
--- a/src/lib/Makefile.am
+++ b/src/lib/Makefile.am
@@ -15,5 +15,8 @@ libreplacements_la_LIBADD = \
 EXTRA_DIST = \
 	replacements.h \
 	clock_gettime.c \
-	clock_gettime.h
-
+	clock_gettime.h \
+	strtok_r.c \
+	strtok_r.h \
+	ffs.c \
+	ffs.h
diff --git a/src/lib/clock_gettime.c b/src/lib/clock_gettime.c
index 77409c71a..054a8c112 100644
--- a/src/lib/clock_gettime.c
+++ b/src/lib/clock_gettime.c
@@ -18,25 +18,25 @@
 
 #include "cvc4_private.h"
 
-#include <stdio.h>
-#include <errno.h>
-#include <time.h>
-
 #include "lib/clock_gettime.h"
 
 #ifdef __cplusplus
 extern "C" {
 #endif /* __cplusplus */
 
-#ifndef __APPLE__
-#  warning This code assumes you're on Mac OS X, and you don't seem to be.  You'll likely have problems.
-#endif /* __APPLE__ */
+#if !(defined(__APPLE__) || defined(__WIN32__))
+#  warning "This code assumes you're on Mac OS X or Win32, and you don't seem to be.  You'll likely have problems."
+#endif /* !(__APPLE__ || __WIN32__) */
 
+#ifdef __APPLE__
+
+#include <stdio.h>
+#include <errno.h>
 #include <mach/mach_time.h>
 
 static double s_clockconv = 0.0;
 
-long clock_gettime(clockid_t which_clock, struct timespec *tp) {
+long clock_gettime(clockid_t which_clock, struct timespec* tp) {
   if( s_clockconv == 0.0 ) {
     mach_timebase_info_data_t tb;
     kern_return_t err = mach_timebase_info(&tb);
@@ -64,6 +64,24 @@ long clock_gettime(clockid_t which_clock, struct timespec *tp) {
   return 0;
 }
 
+#else /* else we're __WIN32__ */
+
+#include <time.h>
+#include <windows.h>
+
+long clock_gettime(clockid_t which_clock, struct timespec* tp) {
+  if(tp != NULL) {
+    FILETIME ft;
+    GetSystemTimeAsFileTime(&ft);
+    uint64_t nanos = ((((uint64_t)ft.dwHighDateTime) << 32) | ft.dwLowDateTime) * 100;
+    tp->tv_sec = nanos / 1000000000ul;
+    tp->tv_nsec = nanos % 1000000000ul;
+  }
+  return 0;
+}
+
+#endif /* __APPLE__ / __WIN32__ */
+
 #ifdef __cplusplus
 }/* extern "C" */
 #endif /* __cplusplus */
diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h
index ac4ca1f85..6a8dd57ff 100644
--- a/src/lib/clock_gettime.h
+++ b/src/lib/clock_gettime.h
@@ -30,13 +30,34 @@
 
 /* otherwise, we have to define it */
 
+#ifdef __WIN32__
+
+#ifdef __cplusplus
+extern "C" {
+#endif /* __cplusplus */
+
+struct timespec {
+  uint64_t tv_sec;
+  int32_t tv_nsec;
+};/* struct timespec */
+
+#ifdef __cplusplus
+}/* extern "C" */
+#endif /* __cplusplus */
+
+#else /* ! __WIN32__ */
+
 /* get timespec from <time.h> */
 #include <time.h>
 
+#endif /* __WIN32__ */
+
 #ifdef __cplusplus
 extern "C" {
 #endif /* __cplusplus */
 
+struct timespec;
+
 typedef enum {
   CLOCK_REALTIME,
   CLOCK_MONOTONIC,
@@ -44,7 +65,7 @@ typedef enum {
   CLOCK_MONOTONIC_HR
 } clockid_t;
 
-long clock_gettime(clockid_t which_clock, struct timespec *tp);
+long clock_gettime(clockid_t which_clock, struct timespec* tp);
 
 #ifdef __cplusplus
 }/* extern "C" */
@@ -52,4 +73,3 @@ long clock_gettime(clockid_t which_clock, struct timespec *tp);
 
 #endif /* HAVE_CLOCK_GETTIME */
 #endif /*__CVC4__LIB__CLOCK_GETTIME_H */
-
diff --git a/src/lib/ffs.c b/src/lib/ffs.c
new file mode 100644
index 000000000..5c25211ce
--- /dev/null
+++ b/src/lib/ffs.c
@@ -0,0 +1,40 @@
+/*********************                                                        */
+/*! \file ffs.c
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Replacement for ffs() for systems without it (like Win32)
+ **
+ ** Replacement for ffs() for systems without it (like Win32).
+ **/
+
+#include "cvc4_private.h"
+
+#include "lib/ffs.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif /* __cplusplus */
+
+int ffs(int i) {
+  long mask = 0x1;
+  int pos = 1;
+  while(pos <= sizeof(int) * 8) {
+    if((mask & i) != 0) {
+      return pos;
+    }
+    ++pos;
+    mask <<= 1;
+  }
+  return 0;
+}
+
+#ifdef __cplusplus
+}/* extern "C" */
+#endif /* __cplusplus */
diff --git a/src/lib/ffs.h b/src/lib/ffs.h
new file mode 100644
index 000000000..9b038d429
--- /dev/null
+++ b/src/lib/ffs.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file ffs.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Replacement for ffs() for systems without it (like Win32)
+ **
+ ** Replacement for ffs() for systems without it (like Win32).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__LIB__FFS_H
+#define __CVC4__LIB__FFS_H
+
+#ifdef HAVE_FFS
+
+// available in strings.h
+#include <strings.h>
+
+#else /* ! HAVE_FFS */
+
+#include "lib/replacements.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif /* __cplusplus */
+
+int ffs(int i);
+
+#ifdef __cplusplus
+}/* extern "C" */
+#endif /* __cplusplus */
+
+#endif /* HAVE_FFS */
+#endif /* __CVC4__LIB__FFS_H */
diff --git a/src/lib/strtok_r.c b/src/lib/strtok_r.c
new file mode 100644
index 000000000..b8df95359
--- /dev/null
+++ b/src/lib/strtok_r.c
@@ -0,0 +1,41 @@
+/*********************                                                        */
+/*! \file strtok_r.c
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Replacement for strtok_r() for systems without it (like Win32)
+ **
+ ** Replacement for strtok_r() for systems without it (like Win32).
+ **/
+
+#include "cvc4_private.h"
+
+#include "lib/strtok_r.h"
+#include <stdio.h>
+#include <string.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif /* __cplusplus */
+
+char* strtok_r(char *str, const char *delim, char **saveptr) {
+  if(str == NULL) {
+    char* retval = strtok(*saveptr, delim);
+    *saveptr = retval + strlen(retval) + 1;
+    return retval;
+  } else {
+    char* retval = strtok(str, delim);
+    *saveptr = retval + strlen(retval) + 1;
+    return retval;
+  }
+}
+
+#ifdef __cplusplus
+}/* extern "C" */
+#endif /* __cplusplus */
diff --git a/src/lib/strtok_r.h b/src/lib/strtok_r.h
new file mode 100644
index 000000000..6b3387e6b
--- /dev/null
+++ b/src/lib/strtok_r.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file strtok_r.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Replacement for strtok_r() for systems without it (like Win32)
+ **
+ ** Replacement for strtok_r() for systems without it (like Win32).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__LIB__STRTOK_R_H
+#define __CVC4__LIB__STRTOK_R_H
+
+#ifdef HAVE_STRTOK_R
+
+// available in string.h
+#include <string.h>
+
+#else /* ! HAVE_STRTOK_R */
+
+#include "lib/replacements.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif /* __cplusplus */
+
+char* strtok_r(char *str, const char *delim, char **saveptr);
+
+#ifdef __cplusplus
+}/* extern "C" */
+#endif /* __cplusplus */
+
+#endif /* HAVE_STRTOK_R */
+#endif /* __CVC4__LIB__STRTOK_R_H */
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 952951655..64a43eb02 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -41,9 +41,9 @@ pcvc4_LDADD += $(BOOST_THREAD_LIBS) -lpthread
 pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS)
 
 if STATIC_BINARY
-pcvc4_LINK = $(CXXLINK) -all-static
+pcvc4_LINK = $(CXXLINK) -all-static $(pcvc4_LDFLAGS)
 else
-pcvc4_LINK = $(CXXLINK)
+pcvc4_LINK = $(CXXLINK) $(pcvc4_LDFLAGS)
 endif
 endif
 
@@ -87,8 +87,8 @@ clean-local:
 	rm -f $(BUILT_SOURCES)
 
 if STATIC_BINARY
-cvc4_LINK = $(CXXLINK) -all-static
+cvc4_LINK = $(CXXLINK) -all-static $(cvc4_LDFLAGS)
 else
-cvc4_LINK = $(CXXLINK)
+cvc4_LINK = $(CXXLINK) $(cvc4_LDFLAGS)
 endif
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index a9a7ef8c5..b429ad0c2 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -180,6 +180,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
   // important even for muzzled builds (to get result output right)
   *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
+  DumpChannel.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
 
   // Create the expression manager using appropriate options
 # ifndef PORTFOLIO_BUILD
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 5e7436580..9ade23630 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -19,10 +19,15 @@
 #include <cerrno>
 #include <exception>
 #include <string.h>
+
+#ifndef __WIN32__
+
 #include <signal.h>
 #include <sys/resource.h>
 #include <unistd.h>
 
+#endif /* __WIN32__ */
+
 #include "util/exception.h"
 #include "options/options.h"
 #include "util/statistics.h"
@@ -44,9 +49,6 @@ namespace CVC4 {
 
 namespace main {
 
-size_t cvc4StackSize;
-void* cvc4StackBase;
-
 /**
  * If true, will not spin on segfault even when CVC4_DEBUG is on.
  * Useful for nightly regressions, noninteractive performance runs
@@ -54,6 +56,11 @@ void* cvc4StackBase;
  */
 bool segvNoSpin = false;
 
+#ifndef __WIN32__
+
+size_t cvc4StackSize;
+void* cvc4StackBase;
+
 /** Handler for SIGXCPU, i.e., timeout. */
 void timeout_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by timeout.\n");
@@ -144,10 +151,12 @@ void ill_handler(int sig, siginfo_t* info, void*) {
 #endif /* CVC4_DEBUG */
 }
 
+#endif /* __WIN32__ */
+
 static terminate_handler default_terminator;
 
 void cvc4unexpected() {
-#ifdef CVC4_DEBUG
+#if defined(CVC4_DEBUG) && !defined(__WIN32__)
   fprintf(stderr, "\n"
           "CVC4 threw an \"unexpected\" exception (one that wasn't properly "
           "specified\nin the throws() specifier for the throwing function)."
@@ -204,6 +213,7 @@ void cvc4terminate() {
 
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw(Exception) {
+#ifndef __WIN32__
   stack_t ss;
   ss.ss_sp = malloc(SIGSTKSZ);
   if(ss.ss_sp == NULL) {
@@ -262,6 +272,8 @@ void cvc4_init() throw(Exception) {
     throw Exception(string("sigaction(SIGILL) failure: ") + strerror(errno));
   }
 
+#endif /* __WIN32__ */
+
   set_unexpected(cvc4unexpected);
   default_terminator = set_terminate(cvc4terminate);
 }
diff --git a/src/options/options.h b/src/options/options.h
index 2d49765f3..5f17f5a5c 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -31,7 +31,7 @@
 namespace CVC4 {
 
 namespace options {
-  class OptionsHolder;
+  struct OptionsHolder;
 }/* CVC4::options namespace */
 
 class ExprStream;
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index d7cd8813b..48834d803 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -356,7 +356,7 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
   // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
   optind = 0;
 #if HAVE_DECL_OPTRESET
-  optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
+  optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
 #endif /* HAVE_DECL_OPTRESET */
 
   // find the base name of the program
@@ -386,7 +386,9 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
     Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind << ", extra_argc == " << extra_argc << std::endl;
     if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) {
 #if HAVE_DECL_OPTRESET
-      optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
+      if(optind_ref != &extra_optind) {
+        optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
+      }
 #endif /* HAVE_DECL_OPTRESET */
       old_optind = optind = extra_optind;
       optind_ref = &extra_optind;
@@ -425,7 +427,9 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
     }
     if(c == -1) {
 #if HAVE_DECL_OPTRESET
-      optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
+      if(optind_ref != &main_optind) {
+        optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
+      }
 #endif /* HAVE_DECL_OPTRESET */
       old_optind = optind = main_optind;
       optind_ref = &main_optind;
@@ -457,7 +461,7 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
     switch(c) {
 ${all_modules_option_handlers}
 
-#line 461 "${template}"
+#line 465 "${template}"
 
     case ':':
       // This can be a long or short option, and the way to get at the
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 8987a7572..fbf2b8650 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -63,8 +63,13 @@ AntlrInputStream*
 AntlrInputStream::newFileInputStream(const std::string& name,
                                      bool useMmap)
   throw (InputStreamException) {
+#ifdef _WIN32
+  if(useMmap) {
+    useMmap = false;
+  }
+#endif
   pANTLR3_INPUT_STREAM input = NULL;
-  if( useMmap ) {
+  if(useMmap) {
     input = MemoryMappedInputBufferNew(name);
   } else {
     // libantlr3c v3.2 isn't source-compatible with v3.4
@@ -74,7 +79,7 @@ AntlrInputStream::newFileInputStream(const std::string& name,
     input = antlr3FileStreamNew((pANTLR3_UINT8) name.c_str(), ANTLR3_ENC_8BIT);
 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
   }
-  if( input == NULL ) {
+  if(input == NULL) {
     throw InputStreamException("Couldn't open file: " + name);
   }
   return new AntlrInputStream( name, input );
diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp
index 9f72ac51c..f110b1145 100644
--- a/src/parser/memory_mapped_input_buffer.cpp
+++ b/src/parser/memory_mapped_input_buffer.cpp
@@ -18,10 +18,15 @@
 #include <stdio.h>
 #include <stdint.h>
 
+#include <antlr3input.h>
+
+#ifndef _WIN32
+
 #include <cerrno>
 #include <sys/mman.h>
 #include <sys/stat.h>
-#include <antlr3input.h>
+
+#endif /* _WIN32 */
 
 #include "parser/memory_mapped_input_buffer.h"
 #include "util/exception.h"
@@ -31,6 +36,14 @@ namespace parser {
 
 extern "C" {
 
+#ifdef _WIN32
+
+pANTLR3_INPUT_STREAM MemoryMappedInputBufferNew(const std::string& filename) {
+  return 0;
+}
+
+#else /* ! _WIN32 */
+
 static ANTLR3_UINT32
 MemoryMapFile(pANTLR3_INPUT_STREAM input, const std::string& filename);
 
@@ -112,6 +125,8 @@ void UnmapFile(pANTLR3_INPUT_STREAM input) {
   input->close(input);
 }
 
+#endif /* _WIN32 */
+
 }/* extern "C" */
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 721dedc70..65d46220b 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -16,6 +16,7 @@
 
 #include <iostream>
 #include <fstream>
+#include <sstream>
 #include <iterator>
 #include <stdint.h>
 #include <cassert>
@@ -500,6 +501,14 @@ Expr Parser::nextExpression() throw(ParserException) {
   return result;
 }
 
+void Parser::attributeNotSupported(const std::string& attr) {
+  if(d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) {
+    stringstream ss;
+    ss << "warning: Attribute " << attr << " not supported (ignoring this and all following uses)";
+    d_input->warning(ss.str());
+    d_attributesWarnedAbout.insert(attr);
+  }
+}
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index fc956b463..958c8a5b5 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -144,6 +144,9 @@ class CVC4_PUBLIC Parser {
   /** The set of operators available in the current logic. */
   std::set<Kind> d_logicOperators;
 
+  /** The set of attributes already warned about. */
+  std::set<std::string> d_attributesWarnedAbout;
+
   /**
    * The current set of unresolved types.  We can get by with this NOT
    * being on the scope, because we can only have one DATATYPE
@@ -451,6 +454,9 @@ public:
     d_input->warning(msg);
   }
 
+  /** Issue a warning to the user, but only once per attribute. */
+  void attributeNotSupported(const std::string& attr);
+
   /** Raise a parse error with the given message. */
   inline void parseError(const std::string& msg) throw(ParserException) {
     d_input->parseError(msg);
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index 6dade9530..0f76baace 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -1,4 +1,3 @@
-/* *******************                                                        */
 /*! \file Smt1.g
  ** \verbatim
  ** Original author: cconway
@@ -235,10 +234,10 @@ annotatedFormula[CVC4::Expr& expr]
   Expr op; /* Operator expression FIXME: move away kill it */
 }
   : /* a built-in operator application */
-    LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK
+    LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr]
     { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
         /* Unary AND/OR can be replaced with the argument.
-	       It just so happens expr should already by the only argument. */
+	 * It just so happens expr should already be the only argument. */
         assert( expr == args[0] );
       } else if( CVC4::kind::isAssociative(kind) &&
                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
@@ -253,6 +252,7 @@ annotatedFormula[CVC4::Expr& expr]
         expr = MK_EXPR(kind, args);
       }
     }
+    termAnnotation[expr]* RPAREN_TOK
 
   | /* A quantifier */
     LPAREN_TOK
@@ -261,12 +261,13 @@ annotatedFormula[CVC4::Expr& expr]
     ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK
       { args.push_back(PARSER_STATE->mkBoundVar(name, t)); }
     )+
-    annotatedFormula[expr] RPAREN_TOK
+    annotatedFormula[expr]
     { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) );
       args2.push_back(expr);
       expr = MK_EXPR(kind, args2);
-      PARSER_STATE->popScope();
     }
+    termAnnotation[expr]* RPAREN_TOK
+    { PARSER_STATE->popScope(); }
 
   | /* A non-built-in function application */
 
@@ -275,9 +276,10 @@ annotatedFormula[CVC4::Expr& expr]
     // { isFunction(LT(2)->getText()) }?
     LPAREN_TOK
     parameterizedOperator[op]
-    annotatedFormulas[args,expr] RPAREN_TOK
+    annotatedFormulas[args,expr]
     // TODO: check arity
     { expr = MK_EXPR(op,args); }
+    termAnnotation[expr]* RPAREN_TOK
 
   | /* An ite expression */
     LPAREN_TOK ITE_TOK
@@ -286,9 +288,9 @@ annotatedFormula[CVC4::Expr& expr]
     annotatedFormula[expr]
     { args.push_back(expr); }
     annotatedFormula[expr]
-    { args.push_back(expr); }
-    RPAREN_TOK
-    { expr = MK_EXPR(CVC4::kind::ITE, args); }
+    { args.push_back(expr);
+      expr = MK_EXPR(CVC4::kind::ITE, args); }
+    termAnnotation[expr]* RPAREN_TOK
 
   | /* a let/flet binding */
     LPAREN_TOK
@@ -298,7 +300,7 @@ annotatedFormula[CVC4::Expr& expr]
     { PARSER_STATE->pushScope();
       PARSER_STATE->defineVar(name,expr); }
     annotatedFormula[expr]
-    RPAREN_TOK
+    termAnnotation[expr]* RPAREN_TOK
     { PARSER_STATE->popScope(); }
 
     /* constants */
@@ -310,7 +312,7 @@ annotatedFormula[CVC4::Expr& expr]
     { // FIXME: This doesn't work because an SMT rational is not a
       // valid GMP rational string
       expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); }
-  | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK  ']'
+  | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']'
     { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); }
     // NOTE: Theory constants go here
     /* TODO: quantifiers, arithmetic constants */
@@ -320,7 +322,6 @@ annotatedFormula[CVC4::Expr& expr]
       | let_identifier[name,CHECK_DECLARED]
       | flet_identifier[name,CHECK_DECLARED] )
     { expr = PARSER_STATE->getVariable(name); }
-
   ;
 
 /**
@@ -458,7 +459,7 @@ functionSymbol[CVC4::Expr& fun]
  * Matches an attribute name from the input (:attribute_name).
  */
 attribute[std::string& s]
-  :  ATTR_IDENTIFIER
+  : ATTR_IDENTIFIER
     { s = AntlrInput::tokenText($ATTR_IDENTIFIER); }
   ;
 
@@ -555,28 +556,56 @@ status[ CVC4::BenchmarkStatus& status ]
 
 /**
  * Matches an annotation, which is an attribute name, with an optional user
+ * value.
  */
 annotation[CVC4::Command*& smt_command]
 @init {
-  std::string key;
+  std::string key, value;
   smt_command = NULL;
+  std::vector<Expr> pats;
+  Expr pat;
 }
-  : attribute[key]
-    ( USER_VALUE
-      { std::string value = AntlrInput::tokenText($USER_VALUE);
-        assert(*value.begin() == '{');
-        assert(*value.rbegin() == '}');
-        // trim whitespace
-        value.erase(value.begin(), value.begin() + 1);
-        value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
-        value.erase(value.end() - 1);
-        value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), value.end());
-        smt_command = new SetInfoCommand(key.c_str() + 1, value); }
-    )?
-    { if(smt_command == NULL) {
-        smt_command = new EmptyCommand(std::string("annotation: ") + key);
+  : PATTERN_ANNOTATION_BEGIN
+    { PARSER_STATE->warning(":pat not supported here; ignored"); }
+    annotatedFormulas[pats,pat] '}'
+  | attribute[key]
+    ( userValue[value]
+      { smt_command = new SetInfoCommand(key.c_str() + 1, value); }
+    | { smt_command = new EmptyCommand(std::string("annotation: ") + key); }
+    )
+  ;
+
+/**
+ * Matches an annotation, which is an attribute name, with an optional user
+ * value.
+ */
+termAnnotation[CVC4::Expr& expr]
+@init {
+  std::string key, value;
+  std::vector<Expr> pats;
+  Expr pat;
+}
+  : PATTERN_ANNOTATION_BEGIN annotatedFormulas[pats,pat] '}'
+    { if(expr.getKind() == kind::FORALL || expr.getKind() == kind::EXISTS) {
+        pat = MK_EXPR(kind::INST_PATTERN, pats);
+        if(expr.getNumChildren() == 3) {
+          // we have other user patterns attached to the quantifier
+          // already; add this one to the existing list
+          pats = expr[2].getChildren();
+          pats.push_back(pat);
+          expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pats));
+        } else {
+          // this is the only user pattern for the quantifier
+          expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pat));
+        }
+      } else {
+        PARSER_STATE->warning(":pat only supported on quantifiers");
       }
     }
+  | ':pat'
+    { PARSER_STATE->warning("expected an instantiation pattern after :pat"); }
+  | attribute[key] userValue[value]?
+    { PARSER_STATE->attributeNotSupported(key); }
   ;
 
 /**
@@ -752,6 +781,15 @@ FLET_IDENTIFIER
  * only constraint imposed on a user-defined value is that it start
  * with an open brace and end with closed brace.
  */
+userValue[std::string& s]
+  : USER_VALUE
+    { s = AntlrInput::tokenText($USER_VALUE); }
+  ;
+
+PATTERN_ANNOTATION_BEGIN
+  : ':pat' (' ' | '\t' | '\f' | '\r' | '\n')* '{'
+  ;
+
 USER_VALUE
   : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}'
   ;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 87cf2083d..648666091 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -629,7 +629,7 @@ pattern[CVC4::Expr& expr]
     }
   ;
 
-simpleSymbolicExpr[CVC4::SExpr& sexpr]
+simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
 @declarations {
   CVC4::Kind k;
   std::string s;
@@ -647,6 +647,10 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr]
       ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
       sexpr = SExpr(ss.str());
     }
+  ;
+
+simpleSymbolicExpr[CVC4::SExpr& sexpr]
+  : simpleSymbolicExprNoKeyword[sexpr]
   | KEYWORD
     { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
   ;
@@ -715,8 +719,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_EXPR(kind, args);
       }
     }
-  | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK 
-    {     
+  | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
+    {
       if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) {
         std::vector<CVC4::Expr> v;
         Expr e = f.getOperator();
@@ -928,22 +932,31 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
   Expr patexpr;
   std::vector<Expr> patexprs;
   Expr e2;
+  bool hasValue = false;
 }
-: KEYWORD
+  : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )?
   {
     attr = AntlrInput::tokenText($KEYWORD);
-    //EXPR_MANAGER->setNamedAttribute( expr, attr );
-    if( attr==":rewrite-rule" ){
-      //do nothing
-    } else if( attr==":axiom" || attr==":conjecture" ){
+    // EXPR_MANAGER->setNamedAttribute( expr, attr );
+    if(attr == ":rewrite-rule") {
+      if(hasValue) {
+        std::stringstream ss;
+        ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
+        PARSER_STATE->warning(ss.str());
+      }
+      // do nothing
+    } else if(attr == ":axiom" || attr == ":conjecture") {
+      if(hasValue) {
+        std::stringstream ss;
+        ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
+        PARSER_STATE->warning(ss.str());
+      }
       std::string attr_name = attr;
       attr_name.erase( attr_name.begin() );
       Command* c = new SetUserAttributeCommand( attr_name, expr );
       PARSER_STATE->preemptCommand(c);
     } else {
-      std::stringstream ss;
-      ss << "Attribute `" << attr << "' not supported";
-      PARSER_STATE->parseError(ss.str());
+      PARSER_STATE->attributeNotSupported(attr);
     }
   }
   | ATTRIBUTE_PATTERN_TOK LPAREN_TOK ( term[patexpr, e2] { patexprs.push_back( patexpr ); }  )+ RPAREN_TOK
@@ -951,6 +964,11 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       attr = std::string(":pattern");
       retExpr = MK_EXPR(kind::INST_PATTERN, patexprs);
     }
+  | ATTRIBUTE_NO_PATTERN_TOK LPAREN_TOK term[patexpr, e2]+ RPAREN_TOK
+    {
+      attr = std::string(":no-pattern");
+      PARSER_STATE->attributeNotSupported(attr);
+    }
   | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
     {
       attr = std::string(":named");
@@ -1098,7 +1116,7 @@ quantOp[CVC4::Kind& kind]
 @init {
   Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : EXISTS_TOK      { $kind = CVC4::kind::EXISTS; }
+  : EXISTS_TOK    { $kind = CVC4::kind::EXISTS; }
   | FORALL_TOK    { $kind = CVC4::kind::FORALL; }
   ;
 
@@ -1374,6 +1392,7 @@ SIMPLIFY_TOK : 'simplify';
 
 // attributes
 ATTRIBUTE_PATTERN_TOK : ':pattern';
+ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
 ATTRIBUTE_NAMED_TOK : ':named';
 
 // operators (NOTE: theory symbols go here)
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 89150142b..1e40ea63f 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -89,7 +89,7 @@ void Tptp::addTheory(Theory theory) {
 
 
 /* The include are managed in the lexer but called in the parser */
-// Inspired by http://www.antlr.org/api/C/interop.html
+// Inspired by http://www.antlr3.org/api/C/interop.html
 
 bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){
   Debug("parser") << "Including " << fileName << std::endl;
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index f0a936c97..e0d4656f4 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -493,9 +493,15 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     case kind::BITVECTOR_UDIV:
       op << "BVUDIV";
       break;
+    case kind::BITVECTOR_UDIV_TOTAL:
+      op << "BVUDIV_TOTAL";
+      break;
     case kind::BITVECTOR_UREM:
       op << "BVUREM";
       break;
+    case kind::BITVECTOR_UREM_TOTAL:
+      op << "BVUREM_TOTAL";
+      break;
     case kind::BITVECTOR_SDIV:
       op << "BVSDIV";
       break;
@@ -671,7 +677,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       toStream(out, n[1], depth, types, false);
       out << ')';
       // TODO: user patterns?
-      break;
+      return;
     case kind::INST_CONSTANT:
       out << "INST_CONSTANT";
       break;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5985f38ef..000fd2fbf 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -254,7 +254,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::BITVECTOR_SUB: out << "bvsub "; break;
   case kind::BITVECTOR_NEG: out << "bvneg "; break;
   case kind::BITVECTOR_UDIV: out << "bvudiv "; break;
+  case kind::BITVECTOR_UDIV_TOTAL: out << "bvudiv_total "; break;
   case kind::BITVECTOR_UREM: out << "bvurem "; break;
+  case kind::BITVECTOR_UREM_TOTAL: out << "bvurem_total "; break;
   case kind::BITVECTOR_SDIV: out << "bvsdiv "; break;
   case kind::BITVECTOR_SREM: out << "bvsrem "; break;
   case kind::BITVECTOR_SMOD: out << "bvsmod "; break;
@@ -539,6 +541,13 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
 }/* Smt2Printer::toStream(CommandStatus*) */
 
 
+void Smt2Printer::toStream(std::ostream& out, Model& m) const throw() {
+  out << "(model" << std::endl;
+  this->Printer::toStream(out, m);
+  out << ")" << std::endl;
+}
+
+
 void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
   theory::TheoryModel& tm = (theory::TheoryModel&) m;
   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index c6d932457..32a0c94ba 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -30,6 +30,7 @@ namespace smt2 {
 class Smt2Printer : public CVC4::Printer {
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
   void toStream(std::ostream& out, Model& m, const Command* c) const throw();
+  void toStream(std::ostream& out, Model& m) const throw();
 public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index d05fe24a7..c1351c6a2 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -26,7 +26,7 @@ namespace CVC4 {
 bool          ProofManager::isInitialized = false;
 ProofManager* ProofManager::proofManager = NULL;
 
-ProofManager::ProofManager(ProofFormat format = LFSC):
+ProofManager::ProofManager(ProofFormat format):
   d_satProof(NULL),
   d_cnfProof(NULL),
   d_format(format)
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 3bfff1456..91eb2ed99 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -52,7 +52,7 @@ class ProofManager {
   
   static ProofManager* proofManager; 
   static bool isInitialized; 
-  ProofManager(ProofFormat format);
+  ProofManager(ProofFormat format = LFSC);
 public:
   static ProofManager* currentPM();
 
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 978ac8d7b..68969c78b 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -32,7 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "theory/interrupted.h"
 using namespace BVMinisat;
 
-namespace CVC4 {
+namespace BVMinisat {
 
 #define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] "
 
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index e5d876b48..b4807b021 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -130,8 +130,6 @@ public:
 
 };/* class DPLLSatSolverInterface */
 
-}/* CVC4::prop namespace */
-
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
   out << lit.toString();
   return out;
@@ -167,6 +165,7 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
   return out;
 }
 
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROP__SAT_MODULE_H */
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index a3065f29b..a0a6429a8 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -23,6 +23,7 @@
 #include "util/dump.h"
 #include "smt/modal_exception.h"
 #include "smt/smt_engine.h"
+#include "lib/strtok_r.h"
 
 #include <cerrno>
 #include <cstring>
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c82b7ca2c..1d98ce115 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -69,6 +69,7 @@
 #include "theory/arrays/options.h"
 #include "util/sort_inference.h"
 #include "theory/quantifiers/macros.h"
+#include "theory/datatypes/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -631,6 +632,11 @@ void SmtEngine::finalOptionsAreSet() {
     }
   }
 
+  if(options::produceAssignments() && !options::produceModels()) {
+    Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << std::endl;
+    setOption("produce-models", SExpr("true"));
+  }
+
   if(! d_logic.isLocked()) {
     // ensure that our heuristics are properly set up
     setLogicInternal();
@@ -972,6 +978,13 @@ void SmtEngine::setLogicInternal() throw() {
       setOption("check-models", SExpr("false"));
     }
   }
+
+  //datatypes theory should assign values to all datatypes terms if logic is quantified
+  if (d_logic.isQuantified() && d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
+    if( !options::dtForceAssignment.wasSetByUser() ){
+      options::dtForceAssignment.set(true);
+    }
+  }
 }
 
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
@@ -2248,7 +2261,7 @@ void SmtEnginePrivate::processAssertions() {
         collectSkolems((*pos).first, skolemSet, cache);
         collectSkolems((*pos).second, skolemSet, cache);
       }
-      
+
       // We need to ensure:
       // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
       // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
@@ -2438,7 +2451,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
   Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
 
   // Check that SAT results generate a model correctly.
-  if(options::checkModels()){
+  if(options::checkModels()) {
     if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
        (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
       checkModel(/* hard failure iff */ ! r.isUnknown());
@@ -2508,7 +2521,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
   Trace("smt") << "SMT query(" << e << ") ==> " << r << endl;
 
   // Check that SAT results generate a model correctly.
-  if(options::checkModels()){
+  if(options::checkModels()) {
     if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
        (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
       checkModel(/* hard failure iff */ ! r.isUnknown());
@@ -2705,20 +2718,22 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
 
   vector<SExpr> sexprs;
   TypeNode boolType = d_nodeManager->booleanType();
+  TheoryModel* m = d_theoryEngine->getModel();
   for(AssignmentSet::const_iterator i = d_assignments->begin(),
         iend = d_assignments->end();
       i != iend;
       ++i) {
     Assert((*i).getType() == boolType);
 
-    // Normalize
-    Node n = Rewriter::rewrite(*i);
+    // Expand, then normalize
+    hash_map<Node, Node, NodeHashFunction> cache;
+    Node n = d_private->expandDefinitions(*i, cache);
+    n = Rewriter::rewrite(n);
 
     Trace("smt") << "--- getting value of " << n << endl;
-    TheoryModel* m = d_theoryEngine->getModel();
     Node resultNode;
-    if( m ){
-      resultNode = m->getValue( n );
+    if(m != NULL) {
+      resultNode = m->getValue(n);
     }
 
     // type-check the result we got
@@ -2727,12 +2742,12 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
     vector<SExpr> v;
     if((*i).getKind() == kind::APPLY) {
       Assert((*i).getNumChildren() == 0);
-      v.push_back((*i).getOperator().toString());
+      v.push_back(SExpr::Keyword((*i).getOperator().toString()));
     } else {
       Assert((*i).isVar());
-      v.push_back((*i).toString());
+      v.push_back(SExpr::Keyword((*i).toString()));
     }
-    v.push_back(resultNode.toString());
+    v.push_back(SExpr::Keyword(resultNode.toString()));
     sexprs.push_back(v);
   }
   return SExpr(sexprs);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3edcd6872..cdae68d96 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -47,7 +47,7 @@ namespace CVC4 {
 template <bool ref_count> class NodeTemplate;
 typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
-class NodeHashFunction;
+struct NodeHashFunction;
 
 class Command;
 class GetModelCommand;
@@ -77,7 +77,7 @@ namespace smt {
    */
   class DefinedFunction;
 
-  class SmtEngineStatistics;
+  struct SmtEngineStatistics;
   class SmtEnginePrivate;
   class SmtScope;
   class BooleanTermConverter;
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index a367b8599..823b61df5 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -338,7 +338,7 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){
 
     bool isDiv = (k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL);
 
-    Integer result = isDiv ? ni.floorDivideQuotient(di) : ni.floorDivideRemainder(di);
+    Integer result = isDiv ? ni.euclidianDivideQuotient(di) : ni.euclidianDivideRemainder(di);
 
     Node resultNode = mkRationalNode(Rational(result));
     return RewriteResponse(REWRITE_DONE, resultNode);
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 9ae7cd1c2..4ee176cf1 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -19,6 +19,7 @@
 
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arith_static_learner.h"
+#include "theory/arith/options.h"
 
 #include "util/propositional_query.h"
 
@@ -61,6 +62,13 @@ ArithStaticLearner::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues);
 }
 
+void ArithStaticLearner::miplibTrickInsert(Node key, Node value){
+  if(options::arithMLTrick()){
+    d_miplibTrick.insert(key, value);
+  }
+}
+
+
 void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
 
   vector<TNode> workList;
@@ -138,7 +146,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
         TNode var = n[1][0];
         Node current = (d_miplibTrick.find(var)  == d_miplibTrick.end()) ?
           mkBoolNode(false) : d_miplibTrick[var];
-        d_miplibTrick.insert(var, n.orNode(current));
+
+        miplibTrickInsert(var, n.orNode(current));
         Debug("arith::miplib") << "insert " << var  << " const " << n << endl;
       }
     }
@@ -338,7 +347,7 @@ void ArithStaticLearner::postProcess(NodeBuilder<>& learned){
     Result isTaut = PropositionalQuery::isTautology(possibleTaut);
     if(isTaut == Result(Result::VALID)){
       miplibTrick(var, values, learned);
-      d_miplibTrick.insert(var, mkBoolNode(false));
+      miplibTrickInsert(var, mkBoolNode(false));
     }
     ++keyIter;
   }
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 0de28c5ab..041ae6339 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -45,6 +45,7 @@ private:
   // The domain is an implicit list OR(x, OR(y, ..., FALSE ))
   // or FALSE
   CDNodeToNodeListMap d_miplibTrick;
+  void miplibTrickInsert(Node key, Node value);
 
   /**
    * Map from a node to it's minimum and maximum.
diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
index a334e2c3d..39b99d625 100644
--- a/src/theory/arith/delta_rational.cpp
+++ b/src/theory/arith/delta_rational.cpp
@@ -83,23 +83,23 @@ DeltaRationalException::DeltaRationalException(const char* op, const DeltaRation
 DeltaRationalException::~DeltaRationalException() throw () { }
 
 
-Integer DeltaRational::floorDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){
+Integer DeltaRational::euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException){
   if(isIntegral() && y.isIntegral()){
     Integer ti = floor();
     Integer yi = y.floor();
-    return ti.floorDivideQuotient(yi);
+    return ti.euclidianDivideQuotient(yi);
   }else{
-    throw DeltaRationalException("floorDivideQuotient", *this, y);
+    throw DeltaRationalException("euclidianDivideQuotient", *this, y);
   }
 }
 
-Integer DeltaRational::floorDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException){
+Integer DeltaRational::euclidianDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException){
   if(isIntegral() && y.isIntegral()){
     Integer ti = floor();
     Integer yi = y.floor();
-    return ti.floorDivideRemainder(yi);
+    return ti.euclidianDivideRemainder(yi);
   }else{
-    throw DeltaRationalException("floorDivideRemainder", *this, y);
+    throw DeltaRationalException("euclidianDivideRemainder", *this, y);
   }
 }
 
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index dc4202f36..19a16d558 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -236,10 +236,10 @@ public:
   }
 
   /** Only well defined if both this and y are integral. */
-  Integer floorDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException);
+  Integer euclidianDivideQuotient(const DeltaRational& y) const throw(DeltaRationalException);
 
   /** Only well defined if both this and y are integral. */
-  Integer floorDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException);
+  Integer euclidianDivideRemainder(const DeltaRational& y) const throw(DeltaRationalException);
 
 
   std::string toString() const;
diff --git a/src/theory/arith/options b/src/theory/arith/options
index 38cf07251..719c826ae 100644
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -51,4 +51,13 @@ option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite-
  turns on the preprocessing rewrite turning equalities into a conjunction of inequalities
 /turns off the preprocessing rewrite turning equalities into a conjunction of inequalities
 
+option arithMLTrick --enable-miplib-trick/--disable-miplib-trick bool :default false :read-write
+ turns on the preprocessing step of attempting to infer bounds on miplib problems
+/turns off the preprocessing step of attempting to infer bounds on miplib problems
+
+option doCutAllBounded --enable-cut-all-bounded/--disable-cut-all-bounded bool :default false :read-write
+ turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
+/ turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
+
+
 endmodule
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 9a41d8d23..fdb4a8ffa 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -225,7 +225,7 @@ private:
   bool equalSizes();
 
   bool inMaps(ArithVar x) const{
-    return 0 <= x && x < d_mapSize;
+    return x < d_mapSize;
   }
 
 };/* class ArithPartialModel */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index f036e20fd..52f234129 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -88,6 +88,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_deltaComputeCallback(this),
   d_basicVarModelUpdateCallBack(d_simplex),
   d_DELTA_ZERO(0),
+  d_fullCheckCounter(0),
   d_statistics()
 {
 }
@@ -752,8 +753,8 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst
       Assert(elim == Rewriter::rewrite(elim));
 
 
-      static const unsigned MAX_SUB_SIZE = 20;
-      if(false && right.size() > MAX_SUB_SIZE){
+      static const unsigned MAX_SUB_SIZE = 2;
+      if(right.size() > MAX_SUB_SIZE){
         Debug("simplify") << "TheoryArith::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl;
         Debug("simplify") << right.size() << endl;
       }else if(elim.hasSubterm(minVar)){
@@ -1730,6 +1731,20 @@ void TheoryArith::check(Effort effortLevel){
   }
   Assert( d_currentPropagationList.empty());
 
+  if(!emmittedConflictOrSplit && fullEffort(effortLevel)){
+    ++d_fullCheckCounter;
+  }
+  static const int CUT_ALL_BOUNDED_PERIOD = 10;
+  if(!emmittedConflictOrSplit && fullEffort(effortLevel) &&
+     d_fullCheckCounter % CUT_ALL_BOUNDED_PERIOD == 1){
+    vector<Node> lemmas = cutAllBounded();
+    //output the lemmas
+    for(vector<Node>::const_iterator i = lemmas.begin(); i != lemmas.end(); ++i){
+      d_out->lemma(*i);
+      ++(d_statistics.d_externalBranchAndBounds);
+    }
+    emmittedConflictOrSplit = lemmas.size() > 0;
+  }
 
   if(!emmittedConflictOrSplit && fullEffort(effortLevel)){
     emmittedConflictOrSplit = splitDisequalities();
@@ -1776,6 +1791,55 @@ void TheoryArith::check(Effort effortLevel){
   Debug("arith") << "TheoryArith::check end" << std::endl;
 }
 
+Node TheoryArith::branchIntegerVariable(ArithVar x) const {
+  const DeltaRational& d = d_partialModel.getAssignment(x);
+  Assert(!d.isIntegral());
+  const Rational& r = d.getNoninfinitesimalPart();
+  const Rational& i = d.getInfinitesimalPart();
+  Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(x) << "]] is " << r << "[" << i << "]" << endl;
+
+  Assert(! (r.getDenominator() == 1 && i.getNumerator() == 0));
+  Assert(!d.isIntegral());
+  TNode var = d_arithvarNodeMap.asNode(x);
+  Integer floor_d = d.floor();
+
+  Node ub = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
+  Node lb = ub.notNode();
+
+
+  Node lem = NodeManager::currentNM()->mkNode(kind::OR, ub, lb);
+  Trace("integers") << "integers: branch & bound: " << lem << endl;
+  if(d_valuation.isSatLiteral(lem[0])) {
+    Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
+  } else {
+    Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
+  }
+  if(d_valuation.isSatLiteral(lem[1])) {
+    Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
+    } else {
+    Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
+  }
+  return lem;
+}
+
+std::vector<Node> TheoryArith::cutAllBounded() const{
+  vector<Node> lemmas;
+  if(options::doCutAllBounded() && getNumberOfVariables() > 0){
+    for(ArithVar iter = 0; iter != getNumberOfVariables(); ++iter){
+    //Do not include slack variables
+      const DeltaRational& d = d_partialModel.getAssignment(iter);
+      if(isInteger(iter) && !isSlackVariable(iter) &&
+         d_partialModel.hasUpperBound(iter) &&
+         d_partialModel.hasLowerBound(iter) &&
+         !d.isIntegral()){
+        Node lem = branchIntegerVariable(iter);
+        lemmas.push_back(lem);
+      }
+    }
+  }
+  return lemmas;
+}
+
 /** Returns true if the roundRobinBranching() issues a lemma. */
 Node TheoryArith::roundRobinBranch(){
   if(hasIntegerModel()){
@@ -1785,36 +1849,40 @@ Node TheoryArith::roundRobinBranch(){
 
     Assert(isInteger(v));
     Assert(!isSlackVariable(v));
+    return branchIntegerVariable(v);
 
-    const DeltaRational& d = d_partialModel.getAssignment(v);
-    const Rational& r = d.getNoninfinitesimalPart();
-    const Rational& i = d.getInfinitesimalPart();
-    Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(v) << "]] is " << r << "[" << i << "]" << endl;
+    // Assert(isInteger(v));
+    // Assert(!isSlackVariable(v));
 
-    Assert(! (r.getDenominator() == 1 && i.getNumerator() == 0));
-    Assert(!d.isIntegral());
+    // const DeltaRational& d = d_partialModel.getAssignment(v);
+    // const Rational& r = d.getNoninfinitesimalPart();
+    // const Rational& i = d.getInfinitesimalPart();
+    // Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(v) << "]] is " << r << "[" << i << "]" << endl;
 
-    TNode var = d_arithvarNodeMap.asNode(v);
-    Integer floor_d = d.floor();
-    Integer ceil_d = d.ceiling();
+    // Assert(! (r.getDenominator() == 1 && i.getNumerator() == 0));
+    // Assert(!d.isIntegral());
 
-    Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
-    Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkRationalNode(ceil_d)));
+    // TNode var = d_arithvarNodeMap.asNode(v);
+    // Integer floor_d = d.floor();
+    // Integer ceil_d = d.ceiling();
 
+    // Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
+    // Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkRationalNode(ceil_d)));
 
-    Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
-    Trace("integers") << "integers: branch & bound: " << lem << endl;
-    if(d_valuation.isSatLiteral(lem[0])) {
-      Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
-    } else {
-      Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
-    }
-    if(d_valuation.isSatLiteral(lem[1])) {
-      Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
-    } else {
-      Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
-    }
-    return lem;
+
+    // Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
+    // Trace("integers") << "integers: branch & bound: " << lem << endl;
+    // if(d_valuation.isSatLiteral(lem[0])) {
+    //   Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
+    // } else {
+    //   Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
+    // }
+    // if(d_valuation.isSatLiteral(lem[1])) {
+    //   Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
+    // } else {
+    //   Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
+    // }
+    // return lem;
   }
 }
 
@@ -2060,10 +2128,10 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) const throw (DeltaRationalExce
       if(n.getKind() == kind::DIVISION_TOTAL){
         res = numer / denom;
       }else if(n.getKind() == kind::INTS_DIVISION_TOTAL){
-        res = Rational(numer.floorDivideQuotient(denom));
+        res = Rational(numer.euclidianDivideQuotient(denom));
       }else{
         Assert(n.getKind() == kind::INTS_MODULUS_TOTAL);
-        res = Rational(numer.floorDivideRemainder(denom));
+        res = Rational(numer.euclidianDivideRemainder(denom));
       }
       if(isSetup(n)){
         ArithVar var = d_arithvarNodeMap.asArithVar(n);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 7d1150fb1..31f9bfcaf 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -537,6 +537,11 @@ private:
   /** Debugging only routine. Prints the model. */
   void debugPrintModel();
 
+  /** Counts the number of fullCheck calls to arithmetic. */
+  uint32_t d_fullCheckCounter;
+  std::vector<Node> cutAllBounded() const;
+  Node branchIntegerVariable(ArithVar x) const;
+
   /** These fields are designed to be accessible to TheoryArith methods. */
   class Statistics {
   public:
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index bd76dd6d4..3ce9bcb44 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -648,6 +648,17 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
 
   Bits r;
   uDivModRec(a, b, q, r, getSize(node)); 
+  // adding a special case for division by 0
+  std::vector<Node> iszero; 
+  for (unsigned i = 0; i < b.size(); ++i) {
+    iszero.push_back(utils::mkNode(kind::IFF, b[i], utils::mkFalse())); 
+  }
+  Node b_is_0 = utils::mkAnd(iszero); 
+  
+  for (unsigned i = 0; i < q.size(); ++i) {
+    q[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), q[i]);
+    r[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), r[i]);
+  }
 
   // cache the remainder in case we need it later
   Node remainder = mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1]);
@@ -664,6 +675,17 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
 
   Bits q;
   uDivModRec(a, b, q, rem, getSize(node)); 
+  // adding a special case for division by 0
+  std::vector<Node> iszero; 
+  for (unsigned i = 0; i < b.size(); ++i) {
+    iszero.push_back(utils::mkNode(kind::IFF, b[i], utils::mkFalse())); 
+  }
+  Node b_is_0 = utils::mkAnd(iszero); 
+  
+  for (unsigned i = 0; i < q.size(); ++i) {
+    q[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), q[i]);
+    rem[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), rem[i]);
+  }
 
   // cache the quotient in case we need it later
   Node quotient = mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]);
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 8b080d104..498378638 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -207,7 +207,7 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
-  BitVector res = a.unsignedDiv(b);
+  BitVector res = a.unsignedDivTotal(b);
   
   return utils::mkConst(res);
 }
@@ -222,7 +222,7 @@ Node RewriteRule<EvalUrem>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl;
   BitVector a = node[0].getConst<BitVector>();
   BitVector b = node[1].getConst<BitVector>();
-  BitVector res = a.unsignedRem(b);
+  BitVector res = a.unsignedRemTotal(b);
   return utils::mkConst(res);
 }
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 23cd8381d..8bcc64414 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -430,10 +430,6 @@ Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
 template<> inline
 bool RewriteRule<XorNot>::applies(TNode node) {
   Unreachable();
-  if (node.getKind() == kind::BITVECTOR_XOR &&
-      node.getNumChildren() == 2 &&
-          node[0].getKind() == kind::BITVECTOR_NOT &&
-          node[1].getKind() == kind::BITVECTOR_NOT); 
 }
 
 template<> inline
diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index 45849858a..1daa30981 100644
--- a/src/theory/datatypes/options
+++ b/src/theory/datatypes/options
@@ -11,5 +11,7 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory
 # cdr( nil ) has no set value.
 expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true
  disable rewriting incorrectly applied selectors to arbitrary ground term
+option dtForceAssignment /--dt-force-assignment bool :default false :read-write
+ force the datatypes solver to give specific values to all datatypes terms before answering sat
  
 endmodule
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index e23d9deae..9e4f0de75 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -24,6 +24,7 @@
 #include "theory/datatypes/theory_datatypes_type_rules.h"
 #include "theory/model.h"
 #include "smt/options.h"
+#include "theory/quantifiers/options.h"
 
 #include <map>
 
@@ -45,7 +46,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"),
   d_selector_apps( c ),
   d_labels( c ),
-  d_conflict( c, false ){
+  d_conflict( c, false ),
+  d_collectTermsCache( c ){
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
@@ -150,7 +152,7 @@ void TheoryDatatypes::check(Effort e) {
                 }
               }
             }
-            if( !needSplit && mustSpecifyModel() ){
+            if( !needSplit && mustSpecifyAssignment() ){
               //for the sake of termination, we must choose the constructor of a ground term
               //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
               //** TODO: this is probably not good enough, actually need fair enumeration strategy
@@ -163,7 +165,7 @@ void TheoryDatatypes::check(Effort e) {
             }
             if( needSplit && consIndex!=-1 ) {
               Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n );
-              Trace("dt-split") << "*************Split for possible constructor " << test << " for " << n <<  endl;
+              Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n <<  endl;
               test = Rewriter::rewrite( test );
               NodeBuilder<> nb(kind::OR);
               nb << test << test.notNode();
@@ -374,8 +376,13 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
 
 void TheoryDatatypes::addSharedTerm(TNode t) {
   Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
-                     << t << endl;
-  d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
+                     << t << " " << t.getType().isBoolean() << endl;
+  if( t.getType().isBoolean() ){
+    //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES);
+  }else{
+    d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
+  }
+  Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
 }
 
 /** propagate */
@@ -488,7 +495,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             Node unifEq = cons1.eqNode( cons2 );
             for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
               if( cons1[i]!=cons2[i] ){
-                Node eq = cons1[i].eqNode( cons2[i] );
+                Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] );
                 d_pending.push_back( eq );
                 d_pending_exp[ eq ] = unifEq;
                 Trace("datatypes-infer") << "DtInfer : " << eq << " by " << unifEq << std::endl;
@@ -758,31 +765,34 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
 
 
 void TheoryDatatypes::collectTerms( Node n ) {
-  for( int i=0; i<(int)n.getNumChildren(); i++ ) {
-    collectTerms( n[i] );
-  }
-  if( n.getKind() == APPLY_CONSTRUCTOR ){
-    //we must take into account subterm relation when checking for cycles
+  if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){
+    d_collectTermsCache[n] = true;
     for( int i=0; i<(int)n.getNumChildren(); i++ ) {
-      Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl;
-      bool result = d_cycle_check.addEdgeNode( n, n[i] );
-      d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
+      collectTerms( n[i] );
     }
-  }else if( n.getKind() == APPLY_SELECTOR ){
-    if( d_selector_apps.find( n )==d_selector_apps.end() ){
-      d_selector_apps[n] = false;
-      //we must also record which selectors exist
-      Debug("datatypes") << "  Found selector " << n << endl;
-      if (n.getType().isBoolean()) {
-        d_equalityEngine.addTriggerPredicate( n );
-      }else{
-        d_equalityEngine.addTerm( n );
+    if( n.getKind() == APPLY_CONSTRUCTOR ){
+      //we must take into account subterm relation when checking for cycles
+      for( int i=0; i<(int)n.getNumChildren(); i++ ) {
+        Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl;
+        bool result = d_cycle_check.addEdgeNode( n, n[i] );
+        d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
       }
-      Node rep = getRepresentative( n[0] );
-      EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
-      if( !eqc->d_selectors ){
-        eqc->d_selectors = true;
-        instantiate( eqc, rep );
+    }else if( n.getKind() == APPLY_SELECTOR ){
+      if( d_selector_apps.find( n )==d_selector_apps.end() ){
+        d_selector_apps[n] = false;
+        //we must also record which selectors exist
+        Debug("datatypes") << "  Found selector " << n << endl;
+        if (n.getType().isBoolean()) {
+          d_equalityEngine.addTriggerPredicate( n );
+        }else{
+          d_equalityEngine.addTerm( n );
+        }
+        Node rep = getRepresentative( n[0] );
+        EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
+        if( !eqc->d_selectors ){
+          eqc->d_selectors = true;
+          instantiate( eqc, rep );
+        }
       }
     }
   }
@@ -793,7 +803,7 @@ void TheoryDatatypes::processNewTerm( Node n ){
   //see if it is rewritten to be something different
   Node rn = Rewriter::rewrite( n );
   if( rn!=n ){
-    Node eq = rn.eqNode( n );
+    Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n );
     d_pending.push_back( eq );
     d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true );
     Trace("datatypes-infer") << "DtInfer : " << eq << ", trivial" << std::endl;
@@ -847,7 +857,7 @@ void TheoryDatatypes::collapseSelectors(){
           Node sn = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, op, cons );
           Node s = Rewriter::rewrite( sn );
           if( sn!=s ){
-            Node eq = s.eqNode( sn );
+            Node eq = s.getType().isBoolean() ? s.iffNode( sn ) : s.eqNode( sn );
             d_pending.push_back( eq );
             d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true );
             Trace("datatypes-infer") << "DtInfer : " << eq << ", by rewrite" << std::endl;
@@ -879,7 +889,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
     int index = getLabelIndex( eqc, n );
     const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
     //must be finite or have a selector
-    if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyModel() ){
+    if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){
       //instantiate this equivalence class
       eqc->d_inst = true;
       Node tt_cons = getInstantiateCons( tt, dt, index );
@@ -963,9 +973,12 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on,
   return false;
 }
 
-bool TheoryDatatypes::mustSpecifyModel(){
-  return options::produceModels();
-  //return options::finiteModelFind() || options::produceModels();
+bool TheoryDatatypes::mustSpecifyAssignment(){
+  //FIXME: the condition finiteModelFind is an over-approximation in this function
+  //   we still may not want to specify assignments for datatypes that are truly infinite
+  //   the fix for this is to correctly compute the cardinality for datatypes containing uninterpered sorts in fmf (i.e. by assuming they are finite)
+  return options::finiteModelFind() || options::produceModels() || options::dtForceAssignment();
+  //return options::produceModels();
   //return false;
 }
 
@@ -976,7 +989,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
   //  (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
   //We may need to communicate (3) outwards if the conclusions involve other theories
   Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
-  if( n.getKind()==EQUAL && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL  ){
+  if( ( n.getKind()==EQUAL || n.getKind()==IFF) && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL  ){
     bool addLemma = false;
 #if 1
     const Datatype& dt = ((DatatypeType)(n[1].getType()).toType()).getDatatype();
@@ -993,13 +1006,15 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
       //check if we have already added this lemma
       if( std::find( d_inst_lemmas[ n[0] ].begin(), d_inst_lemmas[ n[0] ].end(), n[1] )==d_inst_lemmas[ n[0] ].end() ){
         d_inst_lemmas[ n[0] ].push_back( n[1] );
+        Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
         return true;
       }else{
+        Trace("dt-lemma-debug") << "Already communicated " << n << std::endl;
         return false;
       }
     }
-    Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl;
   }
+  Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl;
   return false;
 }
 
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 90d82e255..46212ccbf 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -156,6 +156,8 @@ private:
   context::CDO<bool> d_conflict;
   /** The conflict node */
   Node d_conflictNode;
+  /** cache for which terms we have called collectTerms(...) on */
+  BoolMap d_collectTermsCache;
   /** pending assertions/merges */
   std::vector< Node > d_pending;
   std::map< Node, Node > d_pending_exp;
@@ -234,7 +236,7 @@ private:
     *  This returns true when the datatypes theory is expected to specify the constructor
     *  type for all equivalence classes.
     */
-  bool mustSpecifyModel();
+  bool mustSpecifyAssignment();
   /** must communicate fact */
   bool mustCommunicateFact( Node n, Node exp );
 private:
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index d8557fcaf..2a14d7fba 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -57,6 +57,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
     }
   }
 
+
 public:
 
   DatatypesEnumerator(TypeNode type) throw() :
@@ -91,6 +92,25 @@ public:
     newEnumerators();
   }
 
+  DatatypesEnumerator(const DatatypesEnumerator& other) :
+    TypeEnumeratorBase<DatatypesEnumerator>(other.getType()),
+    d_datatype(other.d_datatype),
+    d_ctor(other.d_ctor),
+    d_zeroCtor(other.d_zeroCtor),
+    d_argEnumerators(NULL) {
+    
+    if (other.d_argEnumerators != NULL) {
+      d_argEnumerators = new TypeEnumerator*[d_datatype[d_ctor].getNumArgs()];
+      for(size_t a = 0; a < d_datatype[d_ctor].getNumArgs(); ++a) {
+        if (other.d_argEnumerators[a] != NULL) {
+          d_argEnumerators[a] = new TypeEnumerator(*other.d_argEnumerators[a]);
+        } else {
+          d_argEnumerators[a] = NULL;
+        }
+       }
+    }             
+  }
+
   ~DatatypesEnumerator() throw() {
     deleteEnumerators();
   }
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 3880aaad9..713587be2 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -77,66 +77,72 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
 
 Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
 {
-  Assert(n.getKind() != kind::FORALL && n.getKind() != kind::EXISTS);
-  if(n.getKind() == kind::LAMBDA) {
-    NodeManager* nm = NodeManager::currentNM();
-    Node body = getModelValue(n[1], true);
-    // This is a bit ugly, but cache inside simplifier can change, so can't be const
-    // The ite simplifier is needed to get rid of artifacts created by Boolean terms
-    body = const_cast<ITESimplifier*>(&d_iteSimp)->simpITE(body);
-    body = Rewriter::rewrite(body);
-    return nm->mkNode(kind::LAMBDA, n[0], body);
-  }
-  if(n.isConst() || (hasBoundVars && n.getKind() == kind::BOUND_VARIABLE)) {
-    return n;
-  }
-
-  TypeNode t = n.getType();
-  if (t.isFunction() || t.isPredicate()) {
-    if (d_enableFuncModels) {
-      std::map< Node, Node >::const_iterator it = d_uf_models.find(n);
-      if (it != d_uf_models.end()) {
-        // Existing function
-        return it->second;
-      }
-      // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type
-      vector<TypeNode> argTypes = t.getArgTypes();
-      vector<Node> args;
+  if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL) {
+    CheckArgument(d_equalityEngine.hasTerm(n), n, "Cannot get the model value for a previously-unseen quantifier: %s", n.toString().c_str());
+  } else {
+    if(n.getKind() == kind::LAMBDA) {
       NodeManager* nm = NodeManager::currentNM();
-      for (unsigned i = 0; i < argTypes.size(); ++i) {
-        args.push_back(nm->mkBoundVar(argTypes[i]));
-      }
-      Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
-      TypeEnumerator te(t.getRangeType());
-      return nm->mkNode(kind::LAMBDA, boundVarList, *te);
+      Node body = getModelValue(n[1], true);
+      // This is a bit ugly, but cache inside simplifier can change, so can't be const
+      // The ite simplifier is needed to get rid of artifacts created by Boolean terms
+      body = const_cast<ITESimplifier*>(&d_iteSimp)->simpITE(body);
+      body = Rewriter::rewrite(body);
+      return nm->mkNode(kind::LAMBDA, n[0], body);
     }
-    // TODO: if func models not enabled, throw an error?
-    Unreachable();
-  }
-
-  if (n.getNumChildren() > 0) {
-    std::vector<Node> children;
-    if (n.getKind() == APPLY_UF) {
-      Node op = getModelValue(n.getOperator(), hasBoundVars);
-      children.push_back(op);
+    if(n.isConst() || (hasBoundVars && n.getKind() == kind::BOUND_VARIABLE)) {
+      return n;
     }
-    else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      children.push_back(n.getOperator());
+
+    TypeNode t = n.getType();
+    if (t.isFunction() || t.isPredicate()) {
+      if (d_enableFuncModels) {
+        std::map< Node, Node >::const_iterator it = d_uf_models.find(n);
+        if (it != d_uf_models.end()) {
+          // Existing function
+          return it->second;
+        }
+        // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type
+        vector<TypeNode> argTypes = t.getArgTypes();
+        vector<Node> args;
+        NodeManager* nm = NodeManager::currentNM();
+        for (unsigned i = 0; i < argTypes.size(); ++i) {
+          args.push_back(nm->mkBoundVar(argTypes[i]));
+        }
+        Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
+        TypeEnumerator te(t.getRangeType());
+        return nm->mkNode(kind::LAMBDA, boundVarList, *te);
+      }
+      // TODO: if func models not enabled, throw an error?
+      Unreachable();
     }
-    //evaluate the children
-    for (unsigned i = 0; i < n.getNumChildren(); ++i) {
-      Node val = getModelValue(n[i], hasBoundVars);
-      children.push_back(val);
+
+    if (n.getNumChildren() > 0) {
+      std::vector<Node> children;
+      if (n.getKind() == APPLY_UF) {
+        Node op = getModelValue(n.getOperator(), hasBoundVars);
+        children.push_back(op);
+      }
+      else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        children.push_back(n.getOperator());
+      }
+      //evaluate the children
+      for (unsigned i = 0; i < n.getNumChildren(); ++i) {
+        Node val = getModelValue(n[i], hasBoundVars);
+        children.push_back(val);
+      }
+      Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children));
+      if(val.getKind() == kind::CARDINALITY_CONSTRAINT) {
+        val = NodeManager::currentNM()->mkConst(getCardinality(val[0].getType().toType()).getFiniteCardinality() <= val[1].getConst<Rational>().getNumerator());
+      }
+      Assert(hasBoundVars || val.isConst());
+      return val;
     }
-    Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children));
-    Assert(hasBoundVars || val.isConst());
-    return val;
-  }
 
-  if (!d_equalityEngine.hasTerm(n)) {
-    // Unknown term - return first enumerated value for this type
-    TypeEnumerator te(n.getType());
-    return *te;
+    if (!d_equalityEngine.hasTerm(n)) {
+      // Unknown term - return first enumerated value for this type
+      TypeEnumerator te(n.getType());
+      return *te;
+    }
   }
   Node val = d_equalityEngine.getRepresentative(n);
   Assert(d_reps.find(val) != d_reps.end());
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 3d98674a8..8272ce168 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -42,10 +42,6 @@ void FirstOrderModel::reset(){
   TheoryModel::reset();
 }
 
-void FirstOrderModel::addTerm( Node n ){
-  TheoryModel::addTerm( n );
-}
-
 void FirstOrderModel::initialize( bool considerAxioms ){
   //rebuild models
   d_uf_model_tree.clear();
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 3779579fd..50a941968 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -33,8 +33,6 @@ class TermDb;
 class FirstOrderModel : public TheoryModel
 {
 private:
-  //add term function
-  void addTerm( Node n );
   //for initialize model
   void initializeModelForTerm( Node n );
   /** whether an axiom is asserted */
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 1a48ec161..dcd7a1b79 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -217,6 +217,88 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, b
 }
 
 
+
+/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
+void CDInstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio ){
+  if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
+    int i_index = imtio ? imtio->d_order[index] : index;
+    Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
+    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+    if( it!=d_data.end() ){
+      it->second->addInstMatch2( qe, f, m, c, index+1, imtio );
+    }else{
+      CDInstMatchTrie* imt = new CDInstMatchTrie( c );
+      d_data[n] = imt;
+      imt->d_valid = true;
+      imt->addInstMatch2( qe, f, m, c, index+1, imtio );
+    }
+  }
+}
+
+/** exists match */
+bool CDInstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){
+  if( !d_valid ){
+    return false;
+  }else if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
+    return true;
+  }else{
+    int i_index = imtio ? imtio->d_order[index] : index;
+    Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
+    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+    if( it!=d_data.end() ){
+      if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
+        return true;
+      }
+    }
+    //check if m is an instance of another instantiation if modInst is true
+    if( modInst ){
+      if( !n.isNull() ){
+        Node nl;
+        it = d_data.find( nl );
+        if( it!=d_data.end() ){
+          if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
+            return true;
+          }
+        }
+      }
+    }
+    if( modEq ){
+      //check modulo equality if any other instantiation match exists
+      if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+        eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
+                                 qe->getEqualityQuery()->getEngine() );
+        while( !eqc.isFinished() ){
+          Node en = (*eqc);
+          if( en!=n ){
+            std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
+            if( itc!=d_data.end() ){
+              if( itc->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
+                return true;
+              }
+            }
+          }
+          ++eqc;
+        }
+      }
+    }
+    return false;
+  }
+}
+
+bool CDInstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
+  return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio );
+}
+
+bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, Context* c, bool modEq, bool modInst, ImtIndexOrder* imtio ){
+  if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){
+    addInstMatch2( qe, f, m, c, 0, imtio );
+    return true;
+  }else{
+    return false;
+  }
+}
+
+
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index c8f843c90..8b2d9726b 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -18,6 +18,7 @@
 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
 
 #include "util/hash.h"
+#include "context/cdo.h"
 
 #include <ext/hash_set>
 #include <map>
@@ -141,6 +142,42 @@ public:
                      bool modInst = false, ImtIndexOrder* imtio = NULL );
 };/* class InstMatchTrie */
 
+
+/** trie for InstMatch objects */
+class CDInstMatchTrie {
+public:
+  class ImtIndexOrder {
+  public:
+    std::vector< int > d_order;
+  };/* class InstMatchTrie ImtIndexOrder */
+private:
+  /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
+  void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio );
+  /** exists match */
+  bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
+public:
+  /** the data */
+  std::map< Node, CDInstMatchTrie* > d_data;
+  /** is valid */
+  context::CDO< bool > d_valid;
+public:
+  CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
+  ~CDInstMatchTrie(){}
+public:
+  /** return true if m exists in this trie
+        modEq is if we check modulo equality
+        modInst is if we return true if m is an instance of a match that exists
+   */
+  bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
+                        bool modInst = false, ImtIndexOrder* imtio = NULL );
+  /** add match m for quantifier f, take into account equalities if modEq = true,
+      if imtio is non-null, this is the order to add to trie
+      return true if successful
+  */
+  bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
+                     bool modInst = false, ImtIndexOrder* imtio = NULL );
+};/* class CDInstMatchTrie */
+
 class InstMatchTrieOrdered{
 private:
   InstMatchTrie::ImtIndexOrder* d_imtio;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index ea22486a6..23f0d8a54 100755
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -87,6 +87,9 @@ private:
   /** generate triggers */

   void generateTriggers( Node f );

 public:

+  /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)

+      rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)

+      rgfr is the frequency at which triggers are generated */

   InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) :

       InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){

     setRegenerateFrequency( rgfr );

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 579c53665..53977ee4f 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -48,8 +48,8 @@ void InstantiationEngine::finishInit(){
     }else{
       d_isup = NULL;
     }
-    InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL,
-                                                                         InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 );
+    int rlv = options::relevantTriggers() ? InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT : InstStrategyAutoGenTriggers::RELEVANCE_NONE;
+    InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, rlv, 3 );
     i_ag->setGenerateAdditional( true );
     addInstStrategy( i_ag );
     //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
@@ -60,11 +60,10 @@ void InstantiationEngine::finishInit(){
     //d_isup->setPriorityOver( i_agm );
     //i_ag->setPriorityOver( i_agm );
   }
-  //CBQI: FIXME
   //for arithmetic
-  //if( options::cbqi() ){
-  //  addInstStrategy( new InstStrategySimplex( d_quantEngine ) );
-  //}
+  if( options::cbqi() ){
+    addInstStrategy( new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ) );
+  }
   //for datatypes
   //if( options::cbqi() ){
   //  addInstStrategy( new InstStrategyDatatypesValue( d_quantEngine ) );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 24d0c4047..bc45e6051 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -44,6 +44,9 @@ option macrosQuant --macros-quant bool :default false
 # Whether to use smart triggers
 option smartTriggers /--disable-smart-triggers bool :default true
  disable smart triggers
+# Whether to use relevent triggers
+option relevantTriggers /--relevant-triggers bool :default true
+ prefer triggers that are more relevant based on SInE style method
 
 # Whether to consider terms in the bodies of quantifiers for matching
 option registerQuantBodyTerms --register-quant-body-terms bool :default false
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 493a49e54..2f6dc47db 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -22,7 +22,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;

 using namespace CVC4::theory::quantifiers;

 

-void QuantifiersAttributes::setUserAttribute( std::string& attr, Node n ){

+void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){

   if( n.getKind()==FORALL ){

     if( attr=="axiom" ){

       Trace("quant-attr") << "Set axiom " << n << std::endl;

diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 822d6c59f..88bac8bc9 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -40,7 +40,7 @@ struct QuantifiersAttributes
     *   This function will apply a custom set of attributes to all top-level universal

     *   quantifiers contained in n

     */

-  static void setUserAttribute( std::string& attr, Node n );

+  static void setUserAttribute( const std::string& attr, Node n );

 };

 

 

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index cfdb30f38..d1dbae90c 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -93,7 +93,15 @@ Node TheoryQuantifiers::getValue(TNode n) {
 }
 
 void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){
-
+  if( fullModel ){
+    for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
+      if((*i).assertion.getKind() == kind::NOT) {
+        m->assertPredicate((*i).assertion[0], false);
+      } else {
+        m->assertPredicate(*i, true);
+      }
+    }
+  }
 }
 
 void TheoryQuantifiers::check(Effort e) {
@@ -192,6 +200,6 @@ bool TheoryQuantifiers::restart(){
   }
 }
 
-void TheoryQuantifiers::setUserAttribute( std::string& attr, Node n ){
+void TheoryQuantifiers::setUserAttribute( const std::string& attr, Node n ){
   QuantifiersAttributes::setUserAttribute( attr, n );
 }
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index c3987144c..b4c8966c7 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -70,7 +70,7 @@ public:
   void shutdown() { }
   std::string identify() const { return std::string("TheoryQuantifiers"); }
   bool flipDecision();
-  void setUserAttribute( std::string& attr, Node n );
+  void setUserAttribute( const std::string& attr, Node n );
   eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
 private:
   void assertUniversal( Node n );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c04920ab8..08bdd496b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -35,9 +35,10 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
-QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te):
+QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
 d_te( te ),
-d_quant_rel( false ){ //currently do not care about relevance
+d_quant_rel( false ),
+d_lemmas_produced_c(u){
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
   d_term_db = new quantifiers::TermDb( this );
   d_tr_trie = new inst::TriggerTrie;
@@ -92,6 +93,10 @@ context::Context* QuantifiersEngine::getSatContext(){
   return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
 }
 
+context::Context* QuantifiersEngine::getUserContext(){
+  return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
+}
+
 OutputChannel& QuantifiersEngine::getOutputChannel(){
   return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
 }
@@ -309,7 +314,7 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
 
 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
   if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
-    if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){
+    if( d_inst_match_trie[f]->existsInstMatch( this, f, m, modEq, modInst ) ){
       return true;
     }
   }
@@ -323,9 +328,9 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b
 bool QuantifiersEngine::addLemma( Node lem ){
   Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
   lem = Rewriter::rewrite(lem);
-  if( d_lemmas_produced.find( lem )==d_lemmas_produced.end() ){
+  if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
     //d_curr_out->lemma( lem );
-    d_lemmas_produced[ lem ] = true;
+    d_lemmas_produced_c[ lem ] = true;
     d_lemmas_waiting.push_back( lem );
     Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl;
     return true;
@@ -355,11 +360,21 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool
     }
   }
   //check for duplication modulo equality
-  if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){
+  inst::CDInstMatchTrie* imt;
+  std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_inst_match_trie.find( f );
+  if( it!=d_inst_match_trie.end() ){
+    imt = it->second;
+  }else{
+    imt = new CDInstMatchTrie( getUserContext() );
+    d_inst_match_trie[f] = imt;
+  }
+  Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+  if( !imt->addInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
     Trace("inst-add-debug") << " -> Already exists." << std::endl;
     ++(d_statistics.d_inst_duplicate);
     return false;
   }
+  Trace("inst-add-debug") << "compute terms" << std::endl;
   //compute the vector of terms for the instantiation
   std::vector< Node > terms;
   for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 8169c78fb..29381a309 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -104,12 +104,13 @@ private:
   std::vector< Node > d_quants;
   /** list of all lemmas produced */
   std::map< Node, bool > d_lemmas_produced;
+  BoolMap d_lemmas_produced_c;
   /** lemmas waiting */
   std::vector< Node > d_lemmas_waiting;
   /** has added lemma this round */
   bool d_hasAddedLemma;
   /** list of all instantiations produced for each quantifier */
-  std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
+  std::map< Node, inst::CDInstMatchTrie* > d_inst_match_trie;
   /** term database */
   quantifiers::TermDb* d_term_db;
   /** all triggers will be stored in this trie */
@@ -121,7 +122,7 @@ private:
 private:
   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
 public:
-  QuantifiersEngine(context::Context* c, TheoryEngine* te);
+  QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
   ~QuantifiersEngine();
   /** get instantiator for id */
   //Instantiator* getInstantiator( theory::TheoryId id );
@@ -136,6 +137,8 @@ public:
   quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
   /** get default sat context for quantifiers engine */
   context::Context* getSatContext();
+  /** get default sat context for quantifiers engine */
+  context::Context* getUserContext();
   /** get default output channel for the quantifiers engine */
   OutputChannel& getOutputChannel();
   /** get default valuation for the quantifiers engine */
diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
index c6fd9611c..a82b94f73 100644
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules.cpp
@@ -276,7 +276,7 @@ void TheoryRewriteRules::check(Effort level) {
       if(glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE)
         continue;
       // If it has a value it should already has been notified
-      bool value; value = value; // avoiding the warning in non debug mode
+      bool value CVC4_UNUSED;
       Assert(!getValuation().hasSatValue(g,value));
       Debug("rewriterules::check") << "RewriteRules::Check Narrowing on:" << g << std::endl;
       /** Can split on already rewritten instrule... but... */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index f317d4b92..5b2032430 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -33,6 +33,7 @@
 #include "options/options.h"
 #include "util/statistics_registry.h"
 #include "util/dump.h"
+#include "lib/ffs.h"
 
 #include <string>
 #include <iostream>
@@ -49,13 +50,13 @@ namespace theory {
 class QuantifiersEngine;
 class TheoryModel;
 
-namespace rrinst{
-class CandidateGenerator;
-}
+namespace rrinst {
+  class CandidateGenerator;
+}/* CVC4::theory::rrinst namespace */
 
 namespace eq {
-class EqualityEngine;
-}
+  class EqualityEngine;
+}/* CVC4::theory::eq namespace */
 
 /**
  * Information about an assertion for the theories.
@@ -786,14 +787,10 @@ public:
   std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
 };/* class Theory */
 
-std::ostream& operator<<(std::ostream& os, Theory::Effort level);
-
-namespace eq{
-  class EqualityEngine;
-}
-
+std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
+inline std::ostream& operator<<(std::ostream& out, const theory::Assertion& a);
 
-inline Assertion Theory::get() {
+inline theory::Assertion Theory::get() {
   Assert( !done(), "Theory::get() called with assertion queue empty!" );
 
   // Get the assertion
@@ -809,7 +806,9 @@ inline Assertion Theory::get() {
   return fact;
 }
 
-}/* CVC4::theory namespace */
+inline std::ostream& operator<<(std::ostream& out, const theory::Assertion& a) {
+  return out << a.assertion;
+}
 
 inline std::ostream& operator<<(std::ostream& out,
                                 const CVC4::theory::Theory& theory) {
@@ -830,6 +829,7 @@ inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertSta
   return out;
 }
 
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__THEORY_H */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c0aa58647..35ed63bed 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -127,7 +127,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   }
 
   // initialize the quantifiers engine
-  d_quantEngine = new QuantifiersEngine(context, this);
+  d_quantEngine = new QuantifiersEngine(context, userContext, this);
 
   // build model information if applicable
   d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true);
@@ -740,8 +740,7 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa
 }
 
 // Recursively traverse a term and call the theory rewriter on its sub-terms
-Node TheoryEngine::ppTheoryRewrite(TNode term)
-{
+Node TheoryEngine::ppTheoryRewrite(TNode term) {
   NodeMap::iterator find = d_ppCache.find(term);
   if (find != d_ppCache.end()) {
     return (*find).second;
@@ -826,7 +825,8 @@ Node TheoryEngine::preprocess(TNode assertion) {
 
     // If this is an atom, we preprocess its terms with the theory ppRewriter
     if (Theory::theoryOf(current) != THEORY_BOOL) {
-      d_ppCache[current] = ppTheoryRewrite(current);
+      Node ppRewritten = ppTheoryRewrite(current);
+      d_ppCache[current] = ppRewritten;
       Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]);
       continue;
     }
@@ -1378,19 +1378,19 @@ void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) {
   d_attr_handle[ str ].push_back( t );
 }
 
-void TheoryEngine::checkTheoryAssertionsWithModel()
-{
-  for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
-    Theory* theory = d_theoryTable[theoryId];
-    if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
-      if (theoryId == THEORY_QUANTIFIERS || theoryId == THEORY_REWRITERULES) {
-        continue;
-      }
-      context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
-      for (unsigned i = 0; it != it_end; ++ it, ++i) {
-        Node assertion = (*it).assertion;
-        Node val = getModel()->getValue(assertion);
-        Assert(val == d_true);
+void TheoryEngine::checkTheoryAssertionsWithModel() {
+  for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
+    if(theoryId != THEORY_REWRITERULES) {
+      Theory* theory = d_theoryTable[theoryId];
+      if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
+        for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
+              it_end = theory->facts_end();
+            it != it_end;
+            ++it) {
+          Node assertion = (*it).assertion;
+          Node val = getModel()->getValue(assertion);
+          Assert(val == d_true);
+        }
       }
     }
   }
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 5df632ff4..c9661c0c7 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -190,22 +190,27 @@ public:
     return d_value.isBitSet(i); 
   }
   
-  BitVector unsignedDiv (const BitVector& y) const {
+  /** 
+   * Total division function that returns 0 when the denominator is 0.  
+   */
+  BitVector unsignedDivTotal (const BitVector& y) const {
+
     CheckArgument(d_size == y.d_size, y);
-    // TODO: decide whether we really want these semantics
     if (y.d_value == 0) {
-      return BitVector(d_size, Integer(0));
+      return BitVector(d_size, 0u);
     }
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value > 0, y);
     return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); 
   }
-
-  BitVector unsignedRem(const BitVector& y) const {
+  
+  /** 
+   * Total division function that returns 0 when the denominator is 0.  
+   */
+  BitVector unsignedRemTotal(const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
-    // TODO: decide whether we really want these semantics
     if (y.d_value == 0) {
-      return BitVector(d_size, d_value);
+      return BitVector(d_size, 0u);
     }
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value > 0, y);
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index e2a8f4a62..81c0428cb 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -285,6 +285,61 @@ public:
   }
 
   /**
+   * Computes a quoitent and remainder according to Boute's Euclidean definition.
+   * euclidianDivideQuotient, euclidianDivideRemainder.
+   *
+   * Boute, Raymond T. (April 1992).
+   * The Euclidean definition of the functions div and mod.
+   * ACM Transactions on Programming Languages and Systems (TOPLAS)
+   * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
+   */
+  static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
+    // compute the floor and then fix the value up if needed.
+    floorQR(q,r,x,y);
+
+    if(r.strictlyNegative()){
+      // if r < 0
+      // abs(r) < abs(y)
+      // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
+      // n = y * q + r
+      // n = y * q - abs(y) + r + abs(y)
+      if(r.sgn() >= 0){
+        // y = abs(y)
+        // n = y * q - y + r + y
+        // n = y * (q-1) + (r+y)
+        q -= 1;
+        r += y;
+      }else{
+        // y = -abs(y)
+        // n = y * q + y + r - y
+        // n = y * (q+1) + (r-y)
+        q += 1;
+        r -= y;
+      }
+    }
+  }
+
+  /**
+   * Returns the quoitent according to Boute's Euclidean definition.
+   * See the documentation for euclidianQR.
+   */
+  Integer euclidianDivideQuotient(const Integer& y) const {
+    Integer q,r;
+    euclidianQR(q,r, *this, y);
+    return q;
+  }
+
+  /**
+   * Returns the remainfing according to Boute's Euclidean definition.
+   * See the documentation for euclidianQR.
+   */
+  Integer euclidianDivideRemainder(const Integer& y) const {
+    Integer q,r;
+    euclidianQR(q,r, *this, y);
+    return r;
+  }
+
+  /**
    * If y divides *this, then exactQuotient returns (this/y)
    */
   Integer exactQuotient(const Integer& y) const {
@@ -381,15 +436,24 @@ public:
     return cln::cl_I_to_int(sgn);
   }
 
-  bool isZero() const {
-    return cln::zerop(d_value);
+
+  inline bool strictlyPositive() const {
+    return sgn() > 0;
+  }
+
+  inline bool strictlyNegative() const {
+    return sgn() < 0;
+  }
+
+  inline bool isZero() const {
+    return sgn() == 0;
   }
 
-  bool isOne() const {
+  inline bool isOne() const {
     return d_value == 1;
   }
 
-  bool isNegativeOne() const {
+  inline bool isNegativeOne() const {
     return d_value == -1;
   }
 
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index d6882b6ac..85d49f921 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -199,16 +199,16 @@ public:
     mpz_class res = d_value;
 
     for (unsigned i = size; i < size + amount; ++i) {
-      mpz_setbit(res.get_mpz_t(), i); 
+      mpz_setbit(res.get_mpz_t(), i);
     }
-    
-    return Integer(res); 
+
+    return Integer(res);
   }
-  
+
   uint32_t toUnsignedInt() const {
     return  mpz_get_ui(d_value.get_mpz_t());
   }
-  
+
   /** See GMP Documentation. */
   Integer extractBitRange(uint32_t bitCount, uint32_t low) const {
     // bitCount = high-low+1
@@ -265,6 +265,61 @@ public:
   }
 
   /**
+   * Computes a quoitent and remainder according to Boute's Euclidean definition.
+   * euclidianDivideQuotient, euclidianDivideRemainder.
+   *
+   * Boute, Raymond T. (April 1992).
+   * The Euclidean definition of the functions div and mod.
+   * ACM Transactions on Programming Languages and Systems (TOPLAS)
+   * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
+   */
+  static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
+    // compute the floor and then fix the value up if needed.
+    floorQR(q,r,x,y);
+
+    if(r.strictlyNegative()){
+      // if r < 0
+      // abs(r) < abs(y)
+      // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
+      // n = y * q + r
+      // n = y * q - abs(y) + r + abs(y)
+      if(r.sgn() >= 0){
+        // y = abs(y)
+        // n = y * q - y + r + y
+        // n = y * (q-1) + (r+y)
+        q -= 1;
+        r += y;
+      }else{
+        // y = -abs(y)
+        // n = y * q + y + r - y
+        // n = y * (q+1) + (r-y)
+        q += 1;
+        r -= y;
+      }
+    }
+  }
+  /**
+   * Returns the quoitent according to Boute's Euclidean definition.
+   * See the documentation for euclidianQR.
+   */
+  Integer euclidianDivideQuotient(const Integer& y) const {
+    Integer q,r;
+    euclidianQR(q,r, *this, y);
+    return q;
+  }
+
+  /**
+   * Returns the remainfing according to Boute's Euclidean definition.
+   * See the documentation for euclidianQR.
+   */
+  Integer euclidianDivideRemainder(const Integer& y) const {
+    Integer q,r;
+    euclidianQR(q,r, *this, y);
+    return r;
+  }
+
+
+  /**
    * If y divides *this, then exactQuotient returns (this/y)
    */
   Integer exactQuotient(const Integer& y) const {
@@ -278,7 +333,7 @@ public:
    * Returns y mod 2^exp
    */
   Integer modByPow2(uint32_t exp) const {
-    mpz_class res; 
+    mpz_class res;
     mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
     return Integer(res);
   }
@@ -292,12 +347,20 @@ public:
     return Integer(res);
   }
 
-  
+
   int sgn() const {
     return mpz_sgn(d_value.get_mpz_t());
   }
 
-  bool isZero() const {
+  inline bool strictlyPositive() const {
+    return sgn() > 0;
+  }
+
+  inline bool strictlyNegative() const {
+    return sgn() < 0;
+  }
+
+  inline bool isZero() const {
     return sgn() == 0;
   }
 
diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h
index e444ba6e2..4c8e646bd 100644
--- a/src/util/node_visitor.h
+++ b/src/util/node_visitor.h
@@ -36,10 +36,11 @@ class NodeVisitor {
   /**
    * Guard against NodeVisitor<> being re-entrant.
    */
+  template <class T>
   class GuardReentry {
-    bool& d_guard;
+    T& d_guard;
   public:
-    GuardReentry(bool& guard)
+    GuardReentry(T& guard)
     : d_guard(guard) {
       Assert(!d_guard);
       d_guard = true;
@@ -71,7 +72,7 @@ public:
    */
   static typename Visitor::return_type run(Visitor& visitor, TNode node) {
 
-    GuardReentry guard(bool(s_inRun));
+    GuardReentry<CVC4_THREADLOCAL_TYPE(bool)> guard(s_inRun);
 
     // Notify of a start
     visitor.start(node);
diff --git a/src/util/record.h b/src/util/record.h
index 2c15d30e0..27b090e1d 100644
--- a/src/util/record.h
+++ b/src/util/record.h
@@ -29,7 +29,7 @@
 
 namespace CVC4 {
 
-class Record;
+class CVC4_PUBLIC Record;
 
 // operators for record select and update
 
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 3bf990dbb..af9088663 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -23,6 +23,7 @@
 
 #include "util/statistics.h"
 #include "util/exception.h"
+#include "lib/clock_gettime.h"
 
 #include <sstream>
 #include <iomanip>
@@ -612,12 +613,17 @@ public:
 
 };/* class StatisticsRegistry */
 
+}/* CVC4 namespace */
+
 /****************************************************************************/
 /* Some utility functions for timespec                                    */
 /****************************************************************************/
 
+inline std::ostream& operator<<(std::ostream& os, const timespec& t);
+
 /** Compute the sum of two timespecs. */
 inline timespec& operator+=(timespec& a, const timespec& b) {
+  using namespace CVC4;
   // assumes a.tv_nsec and b.tv_nsec are in range
   const long nsec_per_sec = 1000000000L; // one thousand million
   CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
@@ -640,6 +646,7 @@ inline timespec& operator+=(timespec& a, const timespec& b) {
 
 /** Compute the difference of two timespecs. */
 inline timespec& operator-=(timespec& a, const timespec& b) {
+  using namespace CVC4;
   // assumes a.tv_nsec and b.tv_nsec are in range
   const long nsec_per_sec = 1000000000L; // one thousand million
   CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
@@ -716,6 +723,8 @@ inline std::ostream& operator<<(std::ostream& os, const timespec& t) {
             << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec;
 }
 
+namespace CVC4 {
+
 class CodeTimer;
 
 /**
@@ -765,7 +774,6 @@ public:
 
 };/* class TimerStat */
 
-
 /**
  * Utility class to make it easier to call stop() at the end of a
  * code block.  When constructed, it starts the timer.  When
@@ -788,7 +796,6 @@ public:
   }
 };/* class CodeTimer */
 
-
 /**
  * To use a statistic, you need to declare it, initialize it in your
  * constructor, register it in your constructor, and deregister it in