12 files changed, 52 insertions, 57 deletions
diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp
index 463cf9534..3da8cfa4a 100644
--- a/examples/api/datatypes.cpp
+++ b/examples/api/datatypes.cpp
@@ -15,8 +15,8 @@
  **/
 
 #include <iostream>
+#include "options/language.h" // for use with make examples
 #include "smt/smt_engine.h" // for use with make examples
-#include "util/language.h" // for use with make examples
 //#include <cvc4/cvc4.h> // To follow the wiki
 
 using namespace CVC4;
diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp
index ad3705a94..e23be29bf 100644
--- a/examples/hashsmt/sha1_collision.cpp
+++ b/examples/hashsmt/sha1_collision.cpp
@@ -29,7 +29,7 @@
 
 #include "word.h"
 #include "sha1.hpp"
-#include "expr/command.h"
+#include "smt_util/command.h"
 
 #include <boost/uuid/sha1.hpp>
 
diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp
index 51267ba06..fadc6ecb9 100644
--- a/examples/hashsmt/sha1_inversion.cpp
+++ b/examples/hashsmt/sha1_inversion.cpp
@@ -29,7 +29,7 @@
 
 #include "word.h"
 #include "sha1.hpp"
-#include "expr/command.h"
+#include "smt_util/command.h"
 
 #include <boost/uuid/sha1.hpp>
 
diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp
index 2dd450c4e..d4aecbba9 100644
--- a/examples/nra-translate/normalize.cpp
+++ b/examples/nra-translate/normalize.cpp
@@ -15,20 +15,19 @@
  ** \todo document this file
  **/
 
-#include <string>
+#include <cassert>
 #include <iostream>
+#include <map>
+#include <string>
 #include <typeinfo>
-#include <cassert>
 #include <vector>
-#include <map>
-
 
-#include "options/options.h"
 #include "expr/expr.h"
-#include "expr/command.h"
+#include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/smt_engine.h"
+#include "smt_util/command.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp
index a2c12f05d..d59f9f4c4 100644
--- a/examples/nra-translate/smt2info.cpp
+++ b/examples/nra-translate/smt2info.cpp
@@ -15,18 +15,17 @@
  ** \todo document this file
  **/
 
-#include <string>
+#include <cassert>
 #include <iostream>
+#include <string>
 #include <typeinfo>
-#include <cassert>
 #include <vector>
 
-
-#include "options/options.h"
 #include "expr/expr.h"
-#include "expr/command.h"
+#include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
+#include "smt_util/command.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp
index 4413c480a..97c5c5d04 100644
--- a/examples/nra-translate/smt2todreal.cpp
+++ b/examples/nra-translate/smt2todreal.cpp
@@ -15,19 +15,19 @@
  ** \todo document this file
  **/
 
-#include <string>
+#include <cassert>
 #include <iostream>
+#include <map>
+#include <string>
 #include <typeinfo>
-#include <cassert>
 #include <vector>
-#include <map>
 
-#include "options/options.h"
 #include "expr/expr.h"
-#include "expr/command.h"
+#include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/smt_engine.h"
+#include "smt_util/command.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp
index eae77e1ce..9c94cdd43 100644
--- a/examples/nra-translate/smt2toisat.cpp
+++ b/examples/nra-translate/smt2toisat.cpp
@@ -15,20 +15,19 @@
  ** \todo document this file
  **/
 
-#include <string>
+#include <cassert>
 #include <iostream>
+#include <map>
+#include <string>
 #include <typeinfo>
-#include <cassert>
 #include <vector>
-#include <map>
-
 
-#include "options/options.h"
 #include "expr/expr.h"
-#include "expr/command.h"
+#include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/smt_engine.h"
+#include "smt_util/command.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp
index 3158243a5..86aaf786f 100644
--- a/examples/nra-translate/smt2tomathematica.cpp
+++ b/examples/nra-translate/smt2tomathematica.cpp
@@ -15,19 +15,18 @@
  ** \todo document this file
  **/
 
-#include <string>
+#include <cassert>
 #include <iostream>
+#include <map>
+#include <string>
 #include <typeinfo>
-#include <cassert>
 #include <vector>
-#include <map>
-
 
-#include "options/options.h"
 #include "expr/expr.h"
-#include "expr/command.h"
+#include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
+#include "smt_util/command.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp
index cb4855a38..058fa8e0d 100644
--- a/examples/nra-translate/smt2toqepcad.cpp
+++ b/examples/nra-translate/smt2toqepcad.cpp
@@ -15,18 +15,18 @@
  ** \todo document this file
  **/
 
-#include <string>
+#include <cassert>
 #include <iostream>
+#include <map>
+#include <string>
 #include <typeinfo>
-#include <cassert>
 #include <vector>
-#include <map>
 
-#include "options/options.h"
 #include "expr/expr.h"
-#include "expr/command.h"
+#include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
+#include "smt_util/command.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp
index 71d7229af..1ebd6ea59 100644
--- a/examples/nra-translate/smt2toredlog.cpp
+++ b/examples/nra-translate/smt2toredlog.cpp
@@ -15,20 +15,19 @@
  ** \todo document this file
  **/
 
-#include <string>
+#include <cassert>
 #include <iostream>
+#include <map>
+#include <string>
 #include <typeinfo>
-#include <cassert>
 #include <vector>
-#include <map>
-
 
-#include "options/options.h"
 #include "expr/expr.h"
-#include "expr/command.h"
+#include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/smt_engine.h"
+#include "smt_util/command.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index acf0fcafe..c33ccb367 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -15,20 +15,19 @@
  ** \todo document this file
  **/
 
-#include <string>
+#include <boost/algorithm/string.hpp> // include Boost, a C++ library
+#include <cassert>
 #include <iostream>
+#include <string>
 #include <typeinfo>
-#include <cassert>
 #include <vector>
-#include <boost/algorithm/string.hpp> // include Boost, a C++ library
 
-
-#include "options/options.h"
 #include "expr/expr.h"
-#include "theory/logic_info.h"
-#include "expr/command.h"
+#include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
+#include "smt_util/command.h"
+#include "theory/logic_info.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/examples/translator.cpp b/examples/translator.cpp
index 7aa969e06..522d88573 100644
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -15,18 +15,19 @@
  ** CVC4's input languages to one of its output languages.
  **/
 
-#include <iostream>
+#include <cerrno>
+#include <cstdlib>
+#include <cstring>
 #include <fstream>
 #include <getopt.h>
-#include <cstring>
-#include <cstdlib>
-#include <cerrno>
-#include "smt/smt_engine.h"
-#include "util/language.h"
-#include "expr/command.h"
+#include <iostream>
+
 #include "expr/expr.h"
-#include "parser/parser_builder.h"
+#include "options/language.h"
 #include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "smt/smt_engine.h"
+#include "smt_util/command.h"
 
 using namespace std;
 using namespace CVC4;