Merge branch 'master' into cleanup-regexp

28 files changed, 464 insertions, 618 deletions

diff --git a/.travis.yml b/.travis.yml
index 1ca15d50e..f474cb47d 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -16,7 +16,6 @@ env:
   #   via the "travis encrypt" command using the project repo's public key
   - secure: "fRfdzYwV10VeW5tVSvy5qpR8ZlkXepR7XWzCulzlHs9SRI2YY20BpzWRjyMBiGu2t7IeJKT7qdjq/CJOQEM8WS76ON7QJ1iymKaRDewDs3OhyPJ71fsFKEGgLky9blk7I9qZh23hnRVECj1oJAVry9IK04bc2zyIEjUYpjRkUAQ="
  matrix:
-  - TRAVIS_CVC4=yes CXXFLAGS='-std=gnu++11' TRAVIS_CVC4_CONFIG='--enable-proof'
   - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c --enable-proof --with-portfolio'
   - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio'
   - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='--disable-proof'
diff --git a/config/is_sorted.m4 b/config/is_sorted.m4
deleted file mode 100644
index 52b062d7e..000000000
--- a/config/is_sorted.m4
+++ /dev/null
@@ -1,20 +0,0 @@
-# CHECK_FOR_IS_SORTED
-# -------------------
-# Look for is_sorted in std:: and __gnu_cxx:: and define
-# some things to make it easy to find later.
-AC_DEFUN([CHECK_FOR_IS_SORTED], [
-AC_MSG_CHECKING([where we can find is_sorted])
-AC_LANG_PUSH([C++])
-is_sorted_result=
-AC_COMPILE_IFELSE([AC_LANG_PROGRAM([#include <algorithm>],
-                                   [std::is_sorted((int*)0L, (int*)0L);])],
-  [is_sorted_result=std],
-  [AC_COMPILE_IFELSE([AC_LANG_PROGRAM([#include <ext/algorithm>],
-                                      [__gnu_cxx::is_sorted((int*)0L, (int*)0L);])],
-    [is_sorted_result=__gnu_cxx],
-    [AC_MSG_FAILURE([cannot find std::is_sorted() or __gnu_cxx::is_sorted()])])])
-AC_LANG_POP([C++])
-AC_MSG_RESULT($is_sorted_result)
-if test "$is_sorted_result" = __gnu_cxx; then is_sorted_result=1; else is_sorted_result=0; fi
-AC_DEFINE_UNQUOTED([IS_SORTED_IN_GNUCXX_NAMESPACE], $is_sorted_result, [Define to 1 if __gnu_cxx::is_sorted() exists])
-])# CHECK_FOR_IS_SORTED
diff --git a/configure.ac b/configure.ac
index b321fef6b..c0cec382f 100644
--- a/configure.ac
+++ b/configure.ac
@@ -1073,9 +1073,6 @@ AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
 # check with which standard strerror_r() complies
 AC_FUNC_STRERROR_R
 
-# is is_sorted() in std or __gnu_cxx?
-CHECK_FOR_IS_SORTED
-
 # require boost library
 BOOST_REQUIRE()
 
diff --git a/examples/hashsmt/sha1.hpp b/examples/hashsmt/sha1.hpp
index 4bfee50fc..72c560dff 100644
--- a/examples/hashsmt/sha1.hpp
+++ b/examples/hashsmt/sha1.hpp
@@ -30,9 +30,9 @@
 // Note: this implementation does not handle message longer than
 //       2^32 bytes.
 
-#pragma once 
+#ifndef __CVC4__EXAMPLES__HASHSMT__SHA1_H
+#define __CVC4__EXAMPLES__HASHSMT__SHA1_H
 
-#include <boost/static_assert.hpp>
 #include <cstddef>
 
 #include "word.h"
@@ -45,8 +45,10 @@ namespace std {
 
 namespace hashsmt {
 
-BOOST_STATIC_ASSERT(sizeof(unsigned char)*8 == 8);
-BOOST_STATIC_ASSERT(sizeof(unsigned int)*8 == 32);
+static_assert(sizeof(unsigned char)*8 == 8,
+              "Unexpected size for unsigned char");
+static_assert(sizeof(unsigned int)*8 == 32,
+              "Unexpected size for unsigned int");
 
 inline cvc4_uint32 left_rotate(cvc4_uint32 x, std::size_t n)
 {
@@ -224,3 +226,4 @@ inline void sha1::get_digest(digest_type digest)
 
 } // namespace hashsmt
 
+#endif /* __CVC4__EXAMPLES__HASHSMT__SHA1_H */
diff --git a/src/base/Makefile.am b/src/base/Makefile.am
index bf919cd81..491baaa90 100644
--- a/src/base/Makefile.am
+++ b/src/base/Makefile.am
@@ -26,9 +26,7 @@ libbase_la_SOURCES = \
 	listener.h \
 	modal_exception.h \
 	output.cpp \
-	output.h \
-	ptr_closer.h
-
+	output.h
 
 
 BUILT_SOURCES = \
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index f989e40e5..93133be24 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -151,7 +151,7 @@ compiled with " + ::CVC4::Configuration::getCompiler() + "\n\
 on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\
 Copyright (c) 2009-2017\n\
 by the authors and their institutional affiliations listed at \n\
-http:\/\/cvc4.cs.stanford.edu/authors\n\n" + \
+http://cvc4.cs.stanford.edu/authors\n\n" + \
     ( IS_GPL_BUILD ? "\
 This build of CVC4 uses GPLed libraries, and is thus covered by the GNU\n\
 General Public License (GPL) version 3.  Versions of CVC4 are available\n\
diff --git a/src/base/ptr_closer.h b/src/base/ptr_closer.h
deleted file mode 100644
index cd0c707b1..000000000
--- a/src/base/ptr_closer.h
+++ /dev/null
@@ -1,73 +0,0 @@
-/*********************                                                        */
-/*! \file ptr_closer.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief A class to close owned pointers in the destructor.
- **
- ** A class to close owned pointers in the destructor.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__PTR_CLOSER_H
-#define __CVC4__PTR_CLOSER_H
-
-namespace CVC4 {
-
-/**
- * A class to close owned pointers in the destructor. This plays a similar role
- * to unique_ptr, but without move semantics. This is designed to overcome the
- * lack of having unique_ptr in C++05.
- *
- * This is a variant of unique_ptr that is not designed for move semantics.
- * These are appropriate to own pointer allocations on the stack that should be
- * deleted when an exception is thrown. These should be used with care within
- * heap based data structures, and never as the return value of a function.
- */
-template <class T>
-class PtrCloser {
- public:
-  PtrCloser() : d_pointer(NULL) {}
-  explicit PtrCloser(T* pointer) : d_pointer(pointer) {}
-  ~PtrCloser() { delete d_pointer; }
-
-  /** Deletes the currently owned copy and takes ownership of pointer. */
-  void reset(T* pointer = NULL) {
-    delete d_pointer;
-    d_pointer = pointer;
-  }
-
-  /** Gives up ownership of the pointer to the caller. */
-  T* release() {
-    T* copy = d_pointer;
-    d_pointer = NULL;
-    return copy;
-  }
-
-  /** Returns the pointer. */
-  T* get() const { return d_pointer; }
-
-  /** Returns the pointer. Undefined if the pointer is null. */
-  T* operator->() const { return d_pointer; }
-
-  /** Returns true if the pointer is not-null. */
-  operator bool() const { return d_pointer != NULL; }
-
- private:
-  PtrCloser(const PtrCloser*) CVC4_UNDEFINED;
-  PtrCloser& operator=(const PtrCloser&) CVC4_UNDEFINED;
-
-  /** An owned pointer object allocated by `new`. Or NULL. */
-  T* d_pointer;
-}; /* class PtrCloser */
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4__PTR_CLOSER_H */
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index f53d60cf9..ef8f661fa 100644
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -33,7 +33,6 @@
 
 #include "cvc4_private.h"
 
-#include <boost/static_assert.hpp>
 #include <deque>
 #include <ext/hash_map>
 #include <utility>
@@ -383,9 +382,8 @@ public:
   }
 };/* class CDInsertHashMap<> */
 
-
 template <class Data, class HashFcn>
-class CDInsertHashMap <TNode, Data, HashFcn > : public ContextObj {
+class CDInsertHashMap<TNode, Data, HashFcn> : public ContextObj {
   /* CDInsertHashMap is challenging to get working with TNode.
    * Consider using CDHashMap<TNode,...> instead.
    *
@@ -397,7 +395,8 @@ class CDInsertHashMap <TNode, Data, HashFcn > : public ContextObj {
    * hashed. Getting the order right with a guarantee is too hard.
    */
 
-  BOOST_STATIC_ASSERT(sizeof(Data) == 0);
+  static_assert(sizeof(Data) == 0,
+                "Cannot create a CDInsertHashMap with TNode keys");
 };
 
 }/* CVC4::context namespace */
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 7cee41b91..3dab675c3 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -20,7 +20,6 @@
 #ifndef __CVC4__CONTEXT__CDLIST_H
 #define __CVC4__CONTEXT__CDLIST_H
 
-#include <boost/static_assert.hpp>
 #include <iterator>
 #include <memory>
 #include <string>
@@ -417,21 +416,21 @@ public:
   }
 };/* class CDList<> */
 
-
 template <class T, class CleanUp>
-class CDList <T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
+class CDList<T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
   /* CDList is incompatible for use with a ContextMemoryAllocator.
    * Consider using CDChunkList<T> instead.
    *
    * Explanation:
-   * If ContextMemoryAllocator is used and d_list grows at a deeper context level
-   * the reallocated will be reallocated in a context memory region that can be
-   * destroyed on pop. To support this, a full copy of d_list would have to be made.
-   * As this is unacceptable for performance in other situations, we do not do
-   * this.
+   * If ContextMemoryAllocator is used and d_list grows at a deeper context
+   * level the reallocated will be reallocated in a context memory region that
+   * can be destroyed on pop. To support this, a full copy of d_list would have
+   * to be made. As this is unacceptable for performance in other situations, we
+   * do not do this.
    */
 
-  BOOST_STATIC_ASSERT(sizeof(T) == 0);
+  static_assert(sizeof(T) == 0,
+                "Cannot create a CDList with a ContextMemoryAllocator.");
 };
 
 }/* CVC4::context namespace */
diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h
index 9f364eac5..0d265271d 100644
--- a/src/context/cdtrail_hashmap.h
+++ b/src/context/cdtrail_hashmap.h
@@ -44,7 +44,6 @@
 
 #pragma once
 
-#include <boost/static_assert.hpp>
 #include <ext/hash_map>
 #include <deque>
 #include <utility>
@@ -551,7 +550,7 @@ public:
 };/* class CDTrailHashMap<> */
 
 template <class Data, class HashFcn>
-class CDTrailHashMap <TNode, Data, HashFcn > : public ContextObj {
+class CDTrailHashMap<TNode, Data, HashFcn> : public ContextObj {
   /* CDTrailHashMap is challenging to get working with TNode.
    * Consider using CDHashMap<TNode,...> instead.
    *
@@ -563,7 +562,8 @@ class CDTrailHashMap <TNode, Data, HashFcn > : public ContextObj {
    * hashed. Getting the order right with a guarantee is too hard.
    */
 
-  BOOST_STATIC_ASSERT(sizeof(Data) == 0);
+  static_assert(sizeof(Data) == 0,
+                "Cannot create a CDTrailHashMap with TNode keys");
 };
 
 }/* CVC4::context namespace */
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 8d8fba43c..57cfa0221 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -155,10 +155,11 @@
 #ifndef __CVC4__NODE_BUILDER_H
 #define __CVC4__NODE_BUILDER_H
 
-#include <iostream>
-#include <vector>
 #include <cstdlib>
+#include <iostream>
+#include <memory>
 #include <stdint.h>
+#include <vector>
 
 namespace CVC4 {
   static const unsigned default_nchild_thresh = 10;
@@ -171,7 +172,6 @@ namespace CVC4 {
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
-#include "base/ptr_closer.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node_value.h"
@@ -890,14 +890,14 @@ template <unsigned nchild_thresh>
 Node* NodeBuilder<nchild_thresh>::constructNodePtr() {
   // maybeCheckType() can throw an exception. Make sure to call the destructor
   // on the exception branch.
-  PtrCloser<Node> np(new Node(constructNV()));
+  std::unique_ptr<Node> np(new Node(constructNV()));
   maybeCheckType(*np.get());
   return np.release();
 }
 
 template <unsigned nchild_thresh>
 Node* NodeBuilder<nchild_thresh>::constructNodePtr() const {
-  PtrCloser<Node> np(new Node(constructNV()));
+  std::unique_ptr<Node> np(new Node(constructNV()));
   maybeCheckType(*np.get());
   return np.release();
 }
diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index 8cccd9bfe..6d655e1fe 100644
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -27,7 +27,7 @@
 namespace CVC4 {
 namespace expr {
 
-class NodeSelfIterator : std::iterator<std::input_iterator_tag, Node> {
+class NodeSelfIterator : public std::iterator<std::input_iterator_tag, Node> {
   Node d_node;
   Node::const_iterator d_child;
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 8b79e046c..697ce6642 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -20,6 +20,7 @@
 #include <cstring>
 #include <fstream>
 #include <iostream>
+#include <memory>
 #include <new>
 
 // This must come before PORTFOLIO_BUILD.
@@ -27,7 +28,6 @@
 
 #include "base/configuration.h"
 #include "base/output.h"
-#include "base/ptr_closer.h"
 #include "expr/expr_iomanip.h"
 #include "expr/expr_manager.h"
 #include "main/command_executor.h"
@@ -249,7 +249,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   }
 # endif
 
-  PtrCloser<Parser> replayParser;
+  std::unique_ptr<Parser> replayParser;
   if( opts.getReplayInputFilename() != "" ) {
     std::string replayFilename = opts.getReplayInputFilename();
     ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts);
@@ -357,7 +357,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
       vector< vector<Command*> > allCommands;
       allCommands.push_back(vector<Command*>());
-      PtrCloser<Parser> parser(parserBuilder.build());
+      std::unique_ptr<Parser> parser(parserBuilder.build());
       if(replayParser) {
         // have the replay parser use the file's declarations
         replayParser->useDeclarationsFrom(parser.get());
@@ -512,7 +512,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
       }
 
-      PtrCloser<Parser> parser(parserBuilder.build());
+      std::unique_ptr<Parser> parser(parserBuilder.build());
       if(replayParser) {
         // have the replay parser use the file's declarations
         replayParser->useDeclarationsFrom(parser.get());
diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp
index ff5d7f7b5..76578b6c4 100644
--- a/src/options/didyoumean_test.cpp
+++ b/src/options/didyoumean_test.cpp
@@ -21,28 +21,28 @@
 
 #include "didyoumean.h"
 #include <iostream>
-#include <boost/foreach.hpp>
+
 using namespace std;
 using namespace CVC4;
 
 set<string> getDebugTags();
 set<string> getOptionStrings();
 
-int main()
-{
+int main() {
   string a, b;
 
   cin >> a;
   cout << "Matches with debug tags:" << endl;
-  vector<string> ret = DidYouMean(getDebugTags()).getMatch(a);
-  BOOST_FOREACH(string s, ret) cout << s << endl;
+  for (const string& s : DidYouMean(getDebugTags()).getMatch(a)) {
+    cout << s << endl;
+  }
   cout << "Matches with option strings:" << endl;
-  ret = DidYouMean(getOptionStrings()).getMatch(a);
-  BOOST_FOREACH(string s, ret) cout << s << endl;
+  for (const string& s : DidYouMean(getOptionStrings()).getMatch(a)) {
+    cout << s << endl;
+  }
 }
 
-set<string> getDebugTags()
-{
+set<string> getDebugTags() {
   set<string> a;
   a.insert("CDInsertHashMap");
   a.insert("CDTrailHashMap");
@@ -426,340 +426,339 @@ set<string> getDebugTags()
   return a;
 }
 
-set<string> getOptionStrings()
-{
+set<string> getOptionStrings() {
   const char* cmdlineOptions[] = {
-    "lang",
-    "output-lang",
-    "language",
-    "output-language",
-    "verbose",
-    "quiet",
-    "stats",
-    "no-stats",
-    "statistics",
-    "no-statistics",
-    "stats-every-query",
-    "no-stats-every-query",
-    "statistics-every-query",
-    "no-statistics-every-query",
-    "parse-only",
-    "no-parse-only",
-    "preprocess-only",
-    "no-preprocess-only",
-    "trace",
-    "debug",
-    "print-success",
-    "no-print-success",
-    "smtlib-strict",
-    "default-expr-depth",
-    "default-dag-thresh",
-    "print-expr-types",
-    "eager-type-checking",
-    "lazy-type-checking",
-    "no-type-checking",
-    "biased-ites",
-    "no-biased-ites",
-    "boolean-term-conversion-mode",
-    "theoryof-mode",
-    "use-theory",
-    "bitblast-eager",
-    "no-bitblast-eager",
-    "bitblast-share-lemmas",
-    "no-bitblast-share-lemmas",
-    "bitblast-eager-fullcheck",
-    "no-bitblast-eager-fullcheck",
-    "bv-inequality-solver",
-    "no-bv-inequality-solver",
-    "bv-core-solver",
-    "no-bv-core-solver",
-    "bv-to-bool",
-    "no-bv-to-bool",
-    "bv-propagate",
-    "no-bv-propagate",
-    "bv-eq",
-    "no-bv-eq",
-    "dt-rewrite-error-sel",
-    "no-dt-rewrite-error-sel",
-    "dt-force-assignment",
-    "unate-lemmas",
-    "arith-prop",
-    "heuristic-pivots",
-    "standard-effort-variable-order-pivots",
-    "error-selection-rule",
-    "simplex-check-period",
-    "pivot-threshold",
-    "prop-row-length",
-    "disable-dio-solver",
-    "enable-arith-rewrite-equalities",
-    "disable-arith-rewrite-equalities",
-    "enable-miplib-trick",
-    "disable-miplib-trick",
-    "miplib-trick-subs",
-    "cut-all-bounded",
-    "no-cut-all-bounded",
-    "maxCutsInContext",
-    "revert-arith-models-on-unsat",
-    "no-revert-arith-models-on-unsat",
-    "fc-penalties",
-    "no-fc-penalties",
-    "use-fcsimplex",
-    "no-use-fcsimplex",
-    "use-soi",
-    "no-use-soi",
-    "restrict-pivots",
-    "no-restrict-pivots",
-    "collect-pivot-stats",
-    "no-collect-pivot-stats",
-    "use-approx",
-    "no-use-approx",
-    "approx-branch-depth",
-    "dio-decomps",
-    "no-dio-decomps",
-    "new-prop",
-    "no-new-prop",
-    "arith-prop-clauses",
-    "soi-qe",
-    "no-soi-qe",
-    "rewrite-divk",
-    "no-rewrite-divk",
-    "se-solve-int",
-    "no-se-solve-int",
-    "lemmas-on-replay-failure",
-    "no-lemmas-on-replay-failure",
-    "dio-turns",
-    "rr-turns",
-    "dio-repeat",
-    "no-dio-repeat",
-    "replay-early-close-depth",
-    "replay-failure-penalty",
-    "replay-num-err-penalty",
-    "replay-reject-cut",
-    "replay-lemma-reject-cut",
-    "replay-soi-major-threshold",
-    "replay-soi-major-threshold-pen",
-    "replay-soi-minor-threshold",
-    "replay-soi-minor-threshold-pen",
-    "symmetry-breaker",
-    "no-symmetry-breaker",
-    "condense-function-values",
-    "no-condense-function-values",
-    "disable-uf-ss-regions",
-    "uf-ss-eager-split",
-    "no-uf-ss-eager-split",
-    "uf-ss-totality",
-    "no-uf-ss-totality",
-    "uf-ss-totality-limited",
-    "uf-ss-totality-sym-break",
-    "no-uf-ss-totality-sym-break",
-    "uf-ss-abort-card",
-    "uf-ss-explained-cliques",
-    "no-uf-ss-explained-cliques",
-    "uf-ss-simple-cliques",
-    "no-uf-ss-simple-cliques",
-    "uf-ss-deq-prop",
-    "no-uf-ss-deq-prop",
-    "disable-uf-ss-min-model",
-    "uf-ss-clique-splits",
-    "no-uf-ss-clique-splits",
-    "uf-ss-sym-break",
-    "no-uf-ss-sym-break",
-    "uf-ss-fair",
-    "no-uf-ss-fair",
-    "arrays-optimize-linear",
-    "no-arrays-optimize-linear",
-    "arrays-lazy-rintro1",
-    "no-arrays-lazy-rintro1",
-    "arrays-model-based",
-    "no-arrays-model-based",
-    "arrays-eager-index",
-    "no-arrays-eager-index",
-    "arrays-eager-lemmas",
-    "no-arrays-eager-lemmas",
-    "disable-miniscope-quant",
-    "disable-miniscope-quant-fv",
-    "disable-prenex-quant",
-    "disable-var-elim-quant",
-    "disable-ite-lift-quant",
-    "cnf-quant",
-    "no-cnf-quant",
-    "clause-split",
-    "no-clause-split",
-    "pre-skolem-quant",
-    "no-pre-skolem-quant",
-    "ag-miniscope-quant",
-    "no-ag-miniscope-quant",
-    "macros-quant",
-    "no-macros-quant",
-    "fo-prop-quant",
-    "no-fo-prop-quant",
-    "disable-smart-triggers",
-    "relevant-triggers",
-    "no-relevant-triggers",
-    "relational-triggers",
-    "no-relational-triggers",
-    "register-quant-body-terms",
-    "no-register-quant-body-terms",
-    "inst-when",
-    "eager-inst-quant",
-    "no-eager-inst-quant",
-    "full-saturate-quant",
-    "no-full-saturate-quant",
-    "literal-matching",
-    "enable-cbqi",
-    "no-enable-cbqi",
-    "cbqi-recurse",
-    "no-cbqi-recurse",
-    "user-pat",
-    "flip-decision",
-    "disable-quant-internal-reps",
-    "finite-model-find",
-    "no-finite-model-find",
-    "mbqi",
-    "mbqi-one-inst-per-round",
-    "no-mbqi-one-inst-per-round",
-    "mbqi-one-quant-per-round",
-    "no-mbqi-one-quant-per-round",
-    "fmf-inst-engine",
-    "no-fmf-inst-engine",
-    "disable-fmf-inst-gen",
-    "fmf-inst-gen-one-quant-per-round",
-    "no-fmf-inst-gen-one-quant-per-round",
-    "fmf-fresh-dc",
-    "no-fmf-fresh-dc",
-    "disable-fmf-fmc-simple",
-    "fmf-bound-int",
-    "no-fmf-bound-int",
-    "axiom-inst",
-    "quant-cf",
-    "no-quant-cf",
-    "quant-cf-mode",
-    "quant-cf-when",
-    "rewrite-rules",
-    "no-rewrite-rules",
-    "rr-one-inst-per-round",
-    "no-rr-one-inst-per-round",
-    "strings-exp",
-    "no-strings-exp",
-    "strings-lb",
-    "strings-fmf",
-    "no-strings-fmf",
-    "strings-eit",
-    "no-strings-eit",
-    "strings-alphabet-card",
-    "show-sat-solvers",
-    "random-freq",
-    "random-seed",
-    "restart-int-base",
-    "restart-int-inc",
-    "refine-conflicts",
-    "no-refine-conflicts",
-    "minisat-elimination",
-    "no-minisat-elimination",
-    "minisat-dump-dimacs",
-    "no-minisat-dump-dimacs",
-    "model-format",
-    "dump",
-    "dump-to",
-    "force-logic",
-    "simplification",
-    "no-simplification",
-    "static-learning",
-    "no-static-learning",
-    "produce-models",
-    "no-produce-models",
-    "check-models",
-    "no-check-models",
-    "dump-models",
-    "no-dump-models",
-    "proof",
-    "no-proof",
-    "check-proofs",
-    "no-check-proofs",
-    "dump-proofs",
-    "no-dump-proofs",
-    "produce-unsat-cores",
-    "no-produce-unsat-cores",
-    "produce-assignments",
-    "no-produce-assignments",
-    "interactive",
-    "no-interactive",
-    "ite-simp",
-    "no-ite-simp",
-    "on-repeat-ite-simp",
-    "no-on-repeat-ite-simp",
-    "simp-with-care",
-    "no-simp-with-care",
-    "simp-ite-compress",
-    "no-simp-ite-compress",
-    "unconstrained-simp",
-    "no-unconstrained-simp",
-    "repeat-simp",
-    "no-repeat-simp",
-    "simp-ite-hunt-zombies",
-    "sort-inference",
-    "no-sort-inference",
-    "incremental",
-    "no-incremental",
-    "abstract-values",
-    "no-abstract-values",
-    "model-u-dt-enum",
-    "no-model-u-dt-enum",
-    "tlimit",
-    "tlimit-per",
-    "rlimit",
-    "rlimit-per",
-    "rewrite-apply-to-const",
-    "no-rewrite-apply-to-const",
-    "replay",
-    "replay-log",
-    "decision",
-    "decision-threshold",
-    "decision-use-weight",
-    "no-decision-use-weight",
-    "decision-random-weight",
-    "decision-weight-internal",
-    "version",
-    "license",
-    "help",
-    "show-config",
-    "show-debug-tags",
-    "show-trace-tags",
-    "early-exit",
-    "no-early-exit",
-    "threads",
-    "threadN",
-    "filter-lemma-length",
-    "fallback-sequential",
-    "no-fallback-sequential",
-    "incremental-parallel",
-    "no-incremental-parallel",
-    "no-interactive-prompt",
-    "continued-execution",
-    "immediate-exit",
-    "segv-spin",
-    "no-segv-spin",
-    "segv-nospin",
-    "wait-to-join",
-    "no-wait-to-join",
-    "strict-parsing",
-    "no-strict-parsing",
-    "mmap",
-    "no-mmap",
-    "no-checking",
-    "no-filesystem-access",
-    "no-include-file",
-    "enable-idl-rewrite-equalities",
-    "disable-idl-rewrite-equalities",
-    "sets-propagate",
-    "no-sets-propagate",
-    "sets-eager-lemmas",
-    "no-sets-eager-lemmas",
-    NULL,
-  };/* cmdlineOptions */
+      "lang",
+      "output-lang",
+      "language",
+      "output-language",
+      "verbose",
+      "quiet",
+      "stats",
+      "no-stats",
+      "statistics",
+      "no-statistics",
+      "stats-every-query",
+      "no-stats-every-query",
+      "statistics-every-query",
+      "no-statistics-every-query",
+      "parse-only",
+      "no-parse-only",
+      "preprocess-only",
+      "no-preprocess-only",
+      "trace",
+      "debug",
+      "print-success",
+      "no-print-success",
+      "smtlib-strict",
+      "default-expr-depth",
+      "default-dag-thresh",
+      "print-expr-types",
+      "eager-type-checking",
+      "lazy-type-checking",
+      "no-type-checking",
+      "biased-ites",
+      "no-biased-ites",
+      "boolean-term-conversion-mode",
+      "theoryof-mode",
+      "use-theory",
+      "bitblast-eager",
+      "no-bitblast-eager",
+      "bitblast-share-lemmas",
+      "no-bitblast-share-lemmas",
+      "bitblast-eager-fullcheck",
+      "no-bitblast-eager-fullcheck",
+      "bv-inequality-solver",
+      "no-bv-inequality-solver",
+      "bv-core-solver",
+      "no-bv-core-solver",
+      "bv-to-bool",
+      "no-bv-to-bool",
+      "bv-propagate",
+      "no-bv-propagate",
+      "bv-eq",
+      "no-bv-eq",
+      "dt-rewrite-error-sel",
+      "no-dt-rewrite-error-sel",
+      "dt-force-assignment",
+      "unate-lemmas",
+      "arith-prop",
+      "heuristic-pivots",
+      "standard-effort-variable-order-pivots",
+      "error-selection-rule",
+      "simplex-check-period",
+      "pivot-threshold",
+      "prop-row-length",
+      "disable-dio-solver",
+      "enable-arith-rewrite-equalities",
+      "disable-arith-rewrite-equalities",
+      "enable-miplib-trick",
+      "disable-miplib-trick",
+      "miplib-trick-subs",
+      "cut-all-bounded",
+      "no-cut-all-bounded",
+      "maxCutsInContext",
+      "revert-arith-models-on-unsat",
+      "no-revert-arith-models-on-unsat",
+      "fc-penalties",
+      "no-fc-penalties",
+      "use-fcsimplex",
+      "no-use-fcsimplex",
+      "use-soi",
+      "no-use-soi",
+      "restrict-pivots",
+      "no-restrict-pivots",
+      "collect-pivot-stats",
+      "no-collect-pivot-stats",
+      "use-approx",
+      "no-use-approx",
+      "approx-branch-depth",
+      "dio-decomps",
+      "no-dio-decomps",
+      "new-prop",
+      "no-new-prop",
+      "arith-prop-clauses",
+      "soi-qe",
+      "no-soi-qe",
+      "rewrite-divk",
+      "no-rewrite-divk",
+      "se-solve-int",
+      "no-se-solve-int",
+      "lemmas-on-replay-failure",
+      "no-lemmas-on-replay-failure",
+      "dio-turns",
+      "rr-turns",
+      "dio-repeat",
+      "no-dio-repeat",
+      "replay-early-close-depth",
+      "replay-failure-penalty",
+      "replay-num-err-penalty",
+      "replay-reject-cut",
+      "replay-lemma-reject-cut",
+      "replay-soi-major-threshold",
+      "replay-soi-major-threshold-pen",
+      "replay-soi-minor-threshold",
+      "replay-soi-minor-threshold-pen",
+      "symmetry-breaker",
+      "no-symmetry-breaker",
+      "condense-function-values",
+      "no-condense-function-values",
+      "disable-uf-ss-regions",
+      "uf-ss-eager-split",
+      "no-uf-ss-eager-split",
+      "uf-ss-totality",
+      "no-uf-ss-totality",
+      "uf-ss-totality-limited",
+      "uf-ss-totality-sym-break",
+      "no-uf-ss-totality-sym-break",
+      "uf-ss-abort-card",
+      "uf-ss-explained-cliques",
+      "no-uf-ss-explained-cliques",
+      "uf-ss-simple-cliques",
+      "no-uf-ss-simple-cliques",
+      "uf-ss-deq-prop",
+      "no-uf-ss-deq-prop",
+      "disable-uf-ss-min-model",
+      "uf-ss-clique-splits",
+      "no-uf-ss-clique-splits",
+      "uf-ss-sym-break",
+      "no-uf-ss-sym-break",
+      "uf-ss-fair",
+      "no-uf-ss-fair",
+      "arrays-optimize-linear",
+      "no-arrays-optimize-linear",
+      "arrays-lazy-rintro1",
+      "no-arrays-lazy-rintro1",
+      "arrays-model-based",
+      "no-arrays-model-based",
+      "arrays-eager-index",
+      "no-arrays-eager-index",
+      "arrays-eager-lemmas",
+      "no-arrays-eager-lemmas",
+      "disable-miniscope-quant",
+      "disable-miniscope-quant-fv",
+      "disable-prenex-quant",
+      "disable-var-elim-quant",
+      "disable-ite-lift-quant",
+      "cnf-quant",
+      "no-cnf-quant",
+      "clause-split",
+      "no-clause-split",
+      "pre-skolem-quant",
+      "no-pre-skolem-quant",
+      "ag-miniscope-quant",
+      "no-ag-miniscope-quant",
+      "macros-quant",
+      "no-macros-quant",
+      "fo-prop-quant",
+      "no-fo-prop-quant",
+      "disable-smart-triggers",
+      "relevant-triggers",
+      "no-relevant-triggers",
+      "relational-triggers",
+      "no-relational-triggers",
+      "register-quant-body-terms",
+      "no-register-quant-body-terms",
+      "inst-when",
+      "eager-inst-quant",
+      "no-eager-inst-quant",
+      "full-saturate-quant",
+      "no-full-saturate-quant",
+      "literal-matching",
+      "enable-cbqi",
+      "no-enable-cbqi",
+      "cbqi-recurse",
+      "no-cbqi-recurse",
+      "user-pat",
+      "flip-decision",
+      "disable-quant-internal-reps",
+      "finite-model-find",
+      "no-finite-model-find",
+      "mbqi",
+      "mbqi-one-inst-per-round",
+      "no-mbqi-one-inst-per-round",
+      "mbqi-one-quant-per-round",
+      "no-mbqi-one-quant-per-round",
+      "fmf-inst-engine",
+      "no-fmf-inst-engine",
+      "disable-fmf-inst-gen",
+      "fmf-inst-gen-one-quant-per-round",
+      "no-fmf-inst-gen-one-quant-per-round",
+      "fmf-fresh-dc",
+      "no-fmf-fresh-dc",
+      "disable-fmf-fmc-simple",
+      "fmf-bound-int",
+      "no-fmf-bound-int",
+      "axiom-inst",
+      "quant-cf",
+      "no-quant-cf",
+      "quant-cf-mode",
+      "quant-cf-when",
+      "rewrite-rules",
+      "no-rewrite-rules",
+      "rr-one-inst-per-round",
+      "no-rr-one-inst-per-round",
+      "strings-exp",
+      "no-strings-exp",
+      "strings-lb",
+      "strings-fmf",
+      "no-strings-fmf",
+      "strings-eit",
+      "no-strings-eit",
+      "strings-alphabet-card",
+      "show-sat-solvers",
+      "random-freq",
+      "random-seed",
+      "restart-int-base",
+      "restart-int-inc",
+      "refine-conflicts",
+      "no-refine-conflicts",
+      "minisat-elimination",
+      "no-minisat-elimination",
+      "minisat-dump-dimacs",
+      "no-minisat-dump-dimacs",
+      "model-format",
+      "dump",
+      "dump-to",
+      "force-logic",
+      "simplification",
+      "no-simplification",
+      "static-learning",
+      "no-static-learning",
+      "produce-models",
+      "no-produce-models",
+      "check-models",
+      "no-check-models",
+      "dump-models",
+      "no-dump-models",
+      "proof",
+      "no-proof",
+      "check-proofs",
+      "no-check-proofs",
+      "dump-proofs",
+      "no-dump-proofs",
+      "produce-unsat-cores",
+      "no-produce-unsat-cores",
+      "produce-assignments",
+      "no-produce-assignments",
+      "interactive",
+      "no-interactive",
+      "ite-simp",
+      "no-ite-simp",
+      "on-repeat-ite-simp",
+      "no-on-repeat-ite-simp",
+      "simp-with-care",
+      "no-simp-with-care",
+      "simp-ite-compress",
+      "no-simp-ite-compress",
+      "unconstrained-simp",
+      "no-unconstrained-simp",
+      "repeat-simp",
+      "no-repeat-simp",
+      "simp-ite-hunt-zombies",
+      "sort-inference",
+      "no-sort-inference",
+      "incremental",
+      "no-incremental",
+      "abstract-values",
+      "no-abstract-values",
+      "model-u-dt-enum",
+      "no-model-u-dt-enum",
+      "tlimit",
+      "tlimit-per",
+      "rlimit",
+      "rlimit-per",
+      "rewrite-apply-to-const",
+      "no-rewrite-apply-to-const",
+      "replay",
+      "replay-log",
+      "decision",
+      "decision-threshold",
+      "decision-use-weight",
+      "no-decision-use-weight",
+      "decision-random-weight",
+      "decision-weight-internal",
+      "version",
+      "license",
+      "help",
+      "show-config",
+      "show-debug-tags",
+      "show-trace-tags",
+      "early-exit",
+      "no-early-exit",
+      "threads",
+      "threadN",
+      "filter-lemma-length",
+      "fallback-sequential",
+      "no-fallback-sequential",
+      "incremental-parallel",
+      "no-incremental-parallel",
+      "no-interactive-prompt",
+      "continued-execution",
+      "immediate-exit",
+      "segv-spin",
+      "no-segv-spin",
+      "segv-nospin",
+      "wait-to-join",
+      "no-wait-to-join",
+      "strict-parsing",
+      "no-strict-parsing",
+      "mmap",
+      "no-mmap",
+      "no-checking",
+      "no-filesystem-access",
+      "no-include-file",
+      "enable-idl-rewrite-equalities",
+      "disable-idl-rewrite-equalities",
+      "sets-propagate",
+      "no-sets-propagate",
+      "sets-eager-lemmas",
+      "no-sets-eager-lemmas",
+      NULL,
+  }; /* cmdlineOptions */
   int i = 0;
   set<string> ret;
-  while(cmdlineOptions[i] != NULL) {
+  while (cmdlineOptions[i] != NULL) {
     ret.insert(cmdlineOptions[i]);
     i++;
   }
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 171c6cab0..a2e9e6f47 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -531,10 +531,10 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 // files. See the documentation in "parser/antlr_undefines.h" for more details.
 #include "parser/antlr_undefines.h"
 
-#include <stdint.h>
 #include <cassert>
+#include <memory>
+#include <stdint.h>
 
-#include "base/ptr_closer.h"
 #include "options/set_language.h"
 #include "parser/antlr_tracing.h"
 #include "parser/parser.h"
@@ -595,7 +595,6 @@ namespace CVC4 {
 #include <vector>
 
 #include "base/output.h"
-#include "base/ptr_closer.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
@@ -659,7 +658,7 @@ parseExpr returns [CVC4::Expr expr = CVC4::Expr()]
  */
 parseCommand returns [CVC4::Command* cmd_return = NULL]
 @declarations {
-    CVC4::PtrCloser<CVC4::Command> cmd;
+    std::unique_ptr<CVC4::Command> cmd;
 }
 @after {
     cmd_return = cmd.release();
@@ -689,7 +688,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL]
  * Matches a command of the input. If a declaration, it will return an empty
  * command.
  */
-command [CVC4::PtrCloser<CVC4::Command>* cmd]
+command [std::unique_ptr<CVC4::Command>* cmd]
   : ( mainCommand[cmd] SEMICOLON
     | SEMICOLON
     | LET_TOK { PARSER_STATE->pushScope(); }
@@ -716,7 +715,7 @@ options { backtrack = true; }
   : letDecl | typeLetDecl[check]
   ;
 
-mainCommand[CVC4::PtrCloser<CVC4::Command>* cmd]
+mainCommand[std::unique_ptr<CVC4::Command>* cmd]
 @init {
   Expr f;
   SExpr sexpr;
@@ -934,7 +933,7 @@ symbolicExpr[CVC4::SExpr& sexpr]
 /**
  * Match a top-level declaration.
  */
-toplevelDeclaration[CVC4::PtrCloser<CVC4::Command>* cmd]
+toplevelDeclaration[std::unique_ptr<CVC4::Command>* cmd]
 @init {
   std::vector<std::string> ids;
   Type t;
@@ -951,7 +950,7 @@ toplevelDeclaration[CVC4::PtrCloser<CVC4::Command>* cmd]
  */
 boundVarDecl[std::vector<std::string>& ids, CVC4::Type& t]
 @init {
-  CVC4::PtrCloser<Command> local_cmd;
+  std::unique_ptr<Command> local_cmd;
 }
   : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON
     declareVariables[&local_cmd,t,ids,false]
@@ -1002,14 +1001,14 @@ boundVarDeclReturn[std::vector<CVC4::Expr>& terms,
  * because type declarations are always top-level, except for
  * type-lets, which don't use this rule.
  */
-declareTypes[CVC4::PtrCloser<CVC4::Command>* cmd,
+declareTypes[std::unique_ptr<CVC4::Command>* cmd,
              const std::vector<std::string>& idList]
 @init {
   Type t;
 }
     /* A sort declaration (e.g., "T : TYPE") */
   : TYPE_TOK
-    { CVC4::PtrCloser<DeclarationSequence> seq(new DeclarationSequence());
+    { std::unique_ptr<DeclarationSequence> seq(new DeclarationSequence());
       for(std::vector<std::string>::const_iterator i = idList.begin();
           i != idList.end(); ++i) {
         // Don't allow a type variable to clash with a previously
@@ -1044,7 +1043,7 @@ declareTypes[CVC4::PtrCloser<CVC4::Command>* cmd,
  * permitted and "cmd" is output.  If topLevel is false, bound vars
  * are created
  */
-declareVariables[CVC4::PtrCloser<CVC4::Command>* cmd, CVC4::Type& t,
+declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::Type& t,
                  const std::vector<std::string>& idList, bool topLevel]
 @init {
   Expr f;
@@ -1052,7 +1051,7 @@ declareVariables[CVC4::PtrCloser<CVC4::Command>* cmd, CVC4::Type& t,
 }
     /* A variable declaration (or definition) */
   : type[t,CHECK_DECLARED] ( EQUAL_TOK formula[f] )?
-    { CVC4::PtrCloser<DeclarationSequence> seq;
+    { std::unique_ptr<DeclarationSequence> seq;
       if(topLevel) {
         seq.reset(new DeclarationSequence());
       }
@@ -2260,7 +2259,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
 constructorDef[CVC4::Datatype& type]
 @init {
   std::string id;
-  CVC4::PtrCloser<CVC4::DatatypeConstructor> ctor;
+  std::unique_ptr<CVC4::DatatypeConstructor> ctor;
 }
   : identifier[id,CHECK_UNDECLARED,SYM_SORT]
     { // make the tester
@@ -2280,7 +2279,7 @@ constructorDef[CVC4::Datatype& type]
     }
   ;
 
-selector[CVC4::PtrCloser<CVC4::DatatypeConstructor>* ctor]
+selector[std::unique_ptr<CVC4::DatatypeConstructor>* ctor]
 @init {
   std::string id;
   Type t, t2;
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index 8f084ba34..ff3308d89 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -4,8 +4,9 @@ AM_CPPFLAGS = \
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable $(WNO_UNINITIALIZED) $(WNO_CONVERSION_NULL)
 
 # Compile generated C files using C++ compiler
-CC=$(CXX)
 AM_CFLAGS = $(AM_CXXFLAGS)
+CFLAGS=$(CXXFLAGS)
+CC=$(CXX)
 
 ANTLR_OPTS =
 
diff --git a/src/parser/smt1/Makefile.am b/src/parser/smt1/Makefile.am
index ae49d0659..f5320002d 100644
--- a/src/parser/smt1/Makefile.am
+++ b/src/parser/smt1/Makefile.am
@@ -5,6 +5,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTH
 
 # Compile generated C files using C++ compiler
 AM_CFLAGS = $(AM_CXXFLAGS)
+CFLAGS=$(CXXFLAGS)
 CC=$(CXX)
 
 ANTLR_OPTS =
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index 315ded475..b30922d58 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -71,9 +71,9 @@ options {
 // files. See the documentation in "parser/antlr_undefines.h" for more details.
 #include "parser/antlr_undefines.h"
 
+#include <memory>
 #include <stdint.h>
 
-#include "base/ptr_closer.h"
 #include "smt/command.h"
 #include "parser/parser.h"
 #include "parser/antlr_tracing.h"
@@ -115,7 +115,6 @@ namespace CVC4 {
 #include <vector>
 
 #include "base/output.h"
-#include "base/ptr_closer.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
@@ -157,7 +156,7 @@ parseExpr returns [CVC4::parser::smt1::myExpr expr]
  */
 parseCommand returns [CVC4::Command* cmd_return = NULL]
 @declarations {
-  CVC4::PtrCloser<CVC4::Command> cmd;
+  std::unique_ptr<CVC4::Command> cmd;
 }
 @after {
   cmd_return = cmd.release();
@@ -177,7 +176,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL]
  * Matches the whole SMT-LIB benchmark.
  * @return the sequence command containing the whole problem
  */
-benchmark [CVC4::PtrCloser<CVC4::Command>* cmd]
+benchmark [std::unique_ptr<CVC4::Command>* cmd]
   : LPAREN_TOK BENCHMARK_TOK IDENTIFIER benchAttributes[cmd] RPAREN_TOK
   | EOF
   ;
@@ -187,10 +186,10 @@ benchmark [CVC4::PtrCloser<CVC4::Command>* cmd]
  * command sequence.
  * @return the command sequence
  */
-benchAttributes [CVC4::PtrCloser<CVC4::Command>* cmd]
+benchAttributes [std::unique_ptr<CVC4::Command>* cmd]
 @init {
-  CVC4::PtrCloser<CVC4::CommandSequence> cmd_seq(new CommandSequence());
-  CVC4::PtrCloser<CVC4::Command> attribute;
+  std::unique_ptr<CVC4::CommandSequence> cmd_seq(new CommandSequence());
+  std::unique_ptr<CVC4::Command> attribute;
 }
 @after {
   cmd->reset(cmd_seq.release());
@@ -205,13 +204,13 @@ benchAttributes [CVC4::PtrCloser<CVC4::Command>* cmd]
  * a corresponding command
  * @return a command corresponding to the attribute
  */
-benchAttribute [CVC4::PtrCloser<CVC4::Command>* smt_command]
+benchAttribute [std::unique_ptr<CVC4::Command>* smt_command]
 @declarations {
   std::string name;
   BenchmarkStatus b_status;
   Expr expr;
-  CVC4::PtrCloser<CVC4::CommandSequence> command_seq;
-  CVC4::PtrCloser<CVC4::Command> declaration_command;
+  std::unique_ptr<CVC4::CommandSequence> command_seq;
+  std::unique_ptr<CVC4::Command> declaration_command;
 }
   : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
     { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name));
@@ -495,7 +494,7 @@ attribute[std::string& s]
     { s = AntlrInput::tokenText($ATTR_IDENTIFIER); }
   ;
 
-functionDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
+functionDeclaration[std::unique_ptr<CVC4::Command>* smt_command]
 @declarations {
   std::string name;
   std::vector<Type> sorts;
@@ -517,7 +516,7 @@ functionDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
 /**
  * Matches the declaration of a predicate and declares it
  */
-predicateDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
+predicateDeclaration[std::unique_ptr<CVC4::Command>* smt_command]
 @declarations {
   std::string name;
   std::vector<Type> p_sorts;
@@ -534,7 +533,7 @@ predicateDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
     }
   ;
 
-sortDeclaration[CVC4::PtrCloser<CVC4::Command>* smt_command]
+sortDeclaration[std::unique_ptr<CVC4::Command>* smt_command]
 @declarations {
   std::string name;
 }
@@ -590,7 +589,7 @@ status[ CVC4::BenchmarkStatus& status ]
  * Matches an annotation, which is an attribute name, with an optional user
  * value.
  */
-annotation[CVC4::PtrCloser<CVC4::Command>* smt_command]
+annotation[std::unique_ptr<CVC4::Command>* smt_command]
 @init {
   std::string key, value;
   std::vector<Expr> pats;
diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am
index fece5e5e8..995e442e6 100644
--- a/src/parser/smt2/Makefile.am
+++ b/src/parser/smt2/Makefile.am
@@ -5,6 +5,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTH
 
 # Compile generated C files using C++ compiler
 AM_CFLAGS = $(AM_CXXFLAGS)
+CFLAGS=$(CXXFLAGS)
 CC=$(CXX)
 
 ANTLR_OPTS =
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 5d24ec024..88709c29a 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -85,7 +85,8 @@ using namespace CVC4::parser;
 // files. See the documentation in "parser/antlr_undefines.h" for more details.
 #include "parser/antlr_undefines.h"
 
-#include "base/ptr_closer.h"
+#include <memory>
+
 #include "parser/parser.h"
 #include "parser/antlr_tracing.h"
 #include "smt/command.h"
@@ -205,7 +206,7 @@ parseExpr returns [CVC4::parser::smt2::myExpr expr]
  */
 parseCommand returns [CVC4::Command* cmd_return = NULL]
 @declarations {
-  CVC4::PtrCloser<CVC4::Command> cmd;
+  std::unique_ptr<CVC4::Command> cmd;
   std::string name;
 }
 @after {
@@ -241,7 +242,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL]
  */
 parseSygus returns [CVC4::Command* cmd_return = NULL]
 @declarations {
-  CVC4::PtrCloser<CVC4::Command> cmd;
+  std::unique_ptr<CVC4::Command> cmd;
   std::string name;
 }
 @after {
@@ -255,7 +256,7 @@ parseSygus returns [CVC4::Command* cmd_return = NULL]
  * Parse the internal portion of the command, ignoring the surrounding
  * parentheses.
  */
-command [CVC4::PtrCloser<CVC4::Command>* cmd]
+command [std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
   std::string name;
   std::vector<std::string> names;
@@ -455,7 +456,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd]
           PARSER_STATE->pushUnsatCoreNameScope();
           cmd->reset(new PushCommand());
         } else {
-          CVC4::PtrCloser<CommandSequence> seq(new CommandSequence());
+          std::unique_ptr<CommandSequence> seq(new CommandSequence());
           do {
             PARSER_STATE->pushScope();
             PARSER_STATE->pushUnsatCoreNameScope();
@@ -495,7 +496,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd]
           PARSER_STATE->popScope();
           cmd->reset(new PopCommand());
         } else {
-          CVC4::PtrCloser<CommandSequence> seq(new CommandSequence());
+          std::unique_ptr<CommandSequence> seq(new CommandSequence());
           do {
             PARSER_STATE->popUnsatCoreNameScope();
             PARSER_STATE->popScope();
@@ -554,7 +555,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd]
     }
   ;
 
-sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
+sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
   std::string name, fun;
   std::vector<std::string> names;
@@ -565,7 +566,7 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
   std::vector<Expr> sygus_vars;
   std::vector<std::pair<std::string, Type> > sortedVarNames;
   SExpr sexpr;
-  CVC4::PtrCloser<CVC4::CommandSequence> seq;
+  std::unique_ptr<CVC4::CommandSequence> seq;
   std::vector< std::vector< CVC4::SygusGTerm > > sgts;
   std::vector< CVC4::Datatype > datatypes;
   std::vector< std::vector<Expr> > ops;
@@ -1075,7 +1076,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
   ;
 
 // Separate this into its own rule (can be invoked by set-info or meta-info)
-metaInfoInternal[CVC4::PtrCloser<CVC4::Command>* cmd]
+metaInfoInternal[std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
   std::string name;
   SExpr sexpr;
@@ -1105,7 +1106,7 @@ metaInfoInternal[CVC4::PtrCloser<CVC4::Command>* cmd]
     }
   ;
 
-setOptionInternal[CVC4::PtrCloser<CVC4::Command>* cmd]
+setOptionInternal[std::unique_ptr<CVC4::Command>* cmd]
 @init {
   std::string name;
   SExpr sexpr;
@@ -1122,7 +1123,7 @@ setOptionInternal[CVC4::PtrCloser<CVC4::Command>* cmd]
     }
   ;
 
-smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd]
+smt25Command[std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
   std::string name;
   std::string fname;
@@ -1136,7 +1137,7 @@ smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd]
   std::vector<Expr> funcs;
   std::vector<Expr> func_defs;
   Expr aexpr;
-  CVC4::PtrCloser<CVC4::CommandSequence> seq;
+  std::unique_ptr<CVC4::CommandSequence> seq;
 }
     /* meta-info */
   : META_INFO_TOK metaInfoInternal[cmd]
@@ -1330,7 +1331,7 @@ smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd]
   // GET_UNSAT_ASSUMPTIONS
   ;
 
-extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd]
+extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
   std::vector<CVC4::Datatype> dts;
   Expr e, e2;
@@ -1340,7 +1341,7 @@ extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd]
   std::vector<Expr> terms;
   std::vector<Type> sorts;
   std::vector<std::pair<std::string, Type> > sortedVarNames;
-  CVC4::PtrCloser<CVC4::CommandSequence> seq;
+  std::unique_ptr<CVC4::CommandSequence> seq;
 }
     /* Extended SMT-LIB set of commands syntax, not permitted in
      * --smtlib2 compliance mode. */
@@ -1495,7 +1496,7 @@ extendedCommand[CVC4::PtrCloser<CVC4::Command>* cmd]
   ;
 
 
-datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd]
+datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
   std::vector<CVC4::Datatype> dts;
   std::string name;
@@ -1515,7 +1516,7 @@ datatypes_2_5_DefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd]
   }
   ;
   
-datatypeDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd]  
+datatypeDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]  
 @declarations {
   std::vector<CVC4::Datatype> dts;
   std::string name;
@@ -1530,7 +1531,7 @@ datatypeDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd]
  { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); }
  ;
   
-datatypesDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd]
+datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
   std::vector<CVC4::Datatype> dts;
   std::string name;
@@ -1593,7 +1594,7 @@ datatypesDefCommand[bool isCo, CVC4::PtrCloser<CVC4::Command>* cmd]
   }
   ;
 
-rewriterulesCommand[CVC4::PtrCloser<CVC4::Command>* cmd]
+rewriterulesCommand[std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
   std::vector<std::pair<std::string, Type> > sortedVarNames;
   std::vector<Expr> args, guards, heads, triggers;
diff --git a/src/parser/tptp/Makefile.am b/src/parser/tptp/Makefile.am
index eab01103f..43bbc595d 100644
--- a/src/parser/tptp/Makefile.am
+++ b/src/parser/tptp/Makefile.am
@@ -5,6 +5,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTH
 
 # Compile generated C files using C++ compiler
 AM_CFLAGS = $(AM_CXXFLAGS)
+CFLAGS=$(CXXFLAGS)
 CC=$(CXX)
 
 ANTLR_OPTS =
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index fe4ea6f98..fbd3d8cfb 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -93,6 +93,8 @@ using namespace CVC4::parser;
 // files. See the documentation in "parser/antlr_undefines.h" for more details.
 #include "parser/antlr_undefines.h"
 
+#include <memory>
+
 #include "smt/command.h"
 #include "parser/parser.h"
 #include "parser/tptp/tptp.h"
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index ef22e1c0d..30b9ca0b5 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -105,11 +105,7 @@ bool Variable::isTranscendentalMember(Node n) {
 
 
 bool VarList::isSorted(iterator start, iterator end) {
-#if IS_SORTED_IN_GNUCXX_NAMESPACE
-  return __gnu_cxx::is_sorted(start, end);
-#else /* IS_SORTED_IN_GNUCXX_NAMESPACE */
   return std::is_sorted(start, end);
-#endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */
 }
 
 bool VarList::isMember(Node n) {
@@ -198,8 +194,7 @@ VarList VarList::operator*(const VarList& other) const {
       otherEnd = other.internalEnd();
 
     Variable::VariableNodeCmp cmp;
-
-    merge_ranges(thisBegin, thisEnd, otherBegin, otherEnd, result, cmp);
+    std::merge(thisBegin, thisEnd, otherBegin, otherEnd, std::back_inserter(result), cmp);
 
     Assert(result.size() >= 2);
     Node mult = NodeManager::currentNM()->mkNode(kind::NONLINEAR_MULT, result);
@@ -356,7 +351,7 @@ void Monomial::printList(const std::vector<Monomial>& list) {
 Polynomial Polynomial::operator+(const Polynomial& vl) const {
 
   std::vector<Monomial> sortedMonos;
-  merge_ranges(begin(), end(), vl.begin(), vl.end(), sortedMonos);
+  std::merge(begin(), end(), vl.begin(), vl.end(), std::back_inserter(sortedMonos));
 
   Monomial::combineAdjacentMonomials(sortedMonos);
   //std::vector<Monomial> combined = Monomial::sumLikeTerms(sortedMonos);
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index d8f5259fc..21301da91 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -23,10 +23,6 @@
 #include <algorithm>
 #include <list>
 
-#if IS_SORTED_IN_GNUCXX_NAMESPACE
-#  include <ext/algorithm>
-#endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */
-
 #include "base/output.h"
 #include "expr/node.h"
 #include "expr/node_self_iterator.h"
@@ -284,7 +280,7 @@ public:
   }
 
   struct VariableNodeCmp {
-    static inline int cmp(Node n, Node m) {
+    static inline int cmp(const Node& n, const Node& m) {
       if ( n == m ) { return 0; }
 
       // this is now slightly off of the old variable order.
@@ -320,7 +316,7 @@ public:
       }
     }
 
-    bool operator()(Node n, Node m) const {
+    bool operator()(const Node& n, const Node& m) const {
       return VariableNodeCmp::cmp(n,m) < 0;
     }
   };
@@ -431,56 +427,6 @@ inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
   return Node(nb);
 }/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
 
-
-template <class GetNodeIterator, class T>
-static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector<T>& result){
-  while(begin != end){
-    result.push_back(*begin);
-    ++begin;
-  }
-}
-
-template <class GetNodeIterator, class T>
-static void merge_ranges(GetNodeIterator first1,
-                  GetNodeIterator last1,
-                  GetNodeIterator first2,
-                  GetNodeIterator last2,
-                  std::vector<T>& result) {
-
-  while(first1 != last1 && first2 != last2){
-    if( (*first1) < (*first2) ){
-      result.push_back(*first1);
-      ++ first1;
-    }else{
-      result.push_back(*first2);
-      ++ first2;
-    }
-  }
-  copy_range(first1, last1, result);
-  copy_range(first2, last2, result);
-}
-
-template <class GetNodeIterator, class T, class Cmp>
-static void merge_ranges(GetNodeIterator first1,
-                         GetNodeIterator last1,
-                         GetNodeIterator first2,
-                         GetNodeIterator last2,
-                         std::vector<T>& result,
-                         const Cmp& cmp) {
-
-  while(first1 != last1 && first2 != last2){
-    if( cmp(*first1, *first2) ){
-      result.push_back(*first1);
-      ++ first1;
-    }else{
-      result.push_back(*first2);
-      ++ first2;
-    }
-  }
-  copy_range(first1, last1, result);
-  copy_range(first2, last2, result);
-}
-
 /**
  * A VarList is a sorted list of variables representing a product.
  * If the VarList is empty, it represents an empty product or 1.
@@ -749,11 +695,7 @@ public:
   }
 
   static bool isSorted(const std::vector<Monomial>& m) {
-#if IS_SORTED_IN_GNUCXX_NAMESPACE
-    return __gnu_cxx::is_sorted(m.begin(), m.end());
-#else /* IS_SORTED_IN_GNUCXX_NAMESPACE */
     return std::is_sorted(m.begin(), m.end());
-#endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */
   }
 
   static bool isStrictlySorted(const std::vector<Monomial>& m) {
@@ -852,7 +794,7 @@ private:
 public:
   static bool isMember(TNode n);
 
-  class iterator {
+  class iterator : public std::iterator<std::input_iterator_tag, Monomial> {
   private:
     internal_iterator d_iter;
 
@@ -954,7 +896,7 @@ public:
     iterator tailStart = begin();
     ++tailStart;
     std::vector<Monomial> subrange;
-    copy_range(tailStart, end(), subrange);
+    std::copy(tailStart, end(), std::back_inserter(subrange));
     return mkPolynomial(subrange);
   }
 
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f70db9823..a2a56e137 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -17,8 +17,6 @@
 #include <algorithm>
 #include "theory/sets/theory_sets_private.h"
 
-#include <boost/foreach.hpp>
-
 #include "expr/emptyset.h"
 #include "options/sets_options.h"
 #include "smt/smt_statistics_registry.h"
@@ -56,7 +54,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
 {
 
   d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external);
-  
+
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
   d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
@@ -79,9 +77,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
 
 TheorySetsPrivate::~TheorySetsPrivate(){
   delete d_rels;
-  for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end(); i != iend; ++i){
-    EqcInfo* current = (*i).second;
-    delete current;
+  for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info) {
+    delete current_pair.second;
   }
 }/* TheorySetsPrivate::~TheorySetsPrivate() */
 
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index cd6f0e11c..877525de7 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -34,6 +34,7 @@ libutil_la_SOURCES = \
 	floatingpoint.h \
 	gmp_util.h \
 	hash.h \
+	index.cpp \
 	index.h \
 	maybe.h \
 	ntuple.h \
diff --git a/src/util/index.cpp b/src/util/index.cpp
new file mode 100644
index 000000000..bd15e2d80
--- /dev/null
+++ b/src/util/index.cpp
@@ -0,0 +1,21 @@
+#include "util/index.h"
+
+#include <cstddef>
+#include <limits>
+
+namespace CVC4 {
+
+static_assert(sizeof(Index) <= sizeof(size_t),
+              "Index cannot be larger than size_t");
+static_assert(!std::numeric_limits<Index>::is_signed,
+              "Index must be unsigned");
+
+/* Discussion: Why is Index a uint32_t instead of size_t (or uint_fast32_t)?
+ *
+ * size_t is a more appropriate choice than uint32_t as the choice is dictated
+ * by uniqueness in arrays and vectors. These correspond to size_t. However, the
+ * using size_t with a sizeof == 8 on 64 bit platforms is noticeably slower.
+ * (Limited testing suggests a ~1/16 of running time.) Interestingly,
+ * uint_fast32_t also has a sizeof == 8 on x86_64.
+ */
+}/* CVC4 namespace */
diff --git a/src/util/index.h b/src/util/index.h
index a8910a696..7329e3f8d 100644
--- a/src/util/index.h
+++ b/src/util/index.h
@@ -9,39 +9,23 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief Standardized type for efficient array indexing.
  **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** Standardized type for efficient array indexing.
  **/
 
 #include "cvc4_private.h"
 
-#pragma once
+#ifndef __CVC4__INDEX_H
+#define __CVC4__INDEX_H
 
-#include <stdint.h>
-#include <boost/static_assert.hpp>
-#include <limits>
+#include <cstdint>
 
 namespace CVC4 {
 
-/**
- * Index is an unsigned integer used for array indexing.
- *
- * This gives a standardized type for independent pieces of code to use as an agreement.
- */
-typedef uint32_t Index;
-
-BOOST_STATIC_ASSERT(sizeof(Index) <= sizeof(size_t));
-BOOST_STATIC_ASSERT(!std::numeric_limits<Index>::is_signed);
-
-/* Discussion: Why is Index a uint32_t instead of size_t (or uint_fast32_t)?
- *
- * size_t is a more appropriate choice than uint32_t as the choice is dictated by
- * uniqueness in arrays and vectors. These correspond to size_t.
- * However, the using size_t with a sizeof == 8 on 64 bit platforms is noticeably
- * slower. (Limited testing suggests a ~1/16 of running time.)
- * (Interestingly, uint_fast32_t also has a sizeof == 8 on x86_64. Filthy Liars!)
- */
+/** Index is a standardized unsigned integer used for efficient indexing. */
+using Index = uint32_t;
 
 }/* CVC4 namespace */
+
+#endif /* __CVC4__INDEX_H */