src/expr/kind.h is now automatically generated.

Build src/expr before src/util.

Moved CVC4::Command to the expr package.

Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).

Added file-level documentation to Antlr sources

When built for debug, spin on SEGV instead of aborting.  Really useful
for debugging problems that crop up only on long runs.  Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.

Updated src/main/about.h for 2010.

23 files changed, 258 insertions, 143 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index fac263152..11173b7e4 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -17,7 +17,7 @@ AM_CPPFLAGS =
 	-I@srcdir@/include -I@srcdir@
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 
-SUBDIRS = util expr context prop smt theory . parser main
+SUBDIRS = expr util context prop smt theory . parser main
 
 lib_LTLIBRARIES = libcvc4.la
 
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 046281702..3212fc0a0 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -15,11 +15,27 @@ libexpr_la_SOURCES = \
 	node_manager.h \
 	expr_manager.h \
 	node_attribute.h \
-	kind.h \
+	@srcdir@/kind.h \
 	node.cpp \
 	node_builder.cpp \
 	node_manager.cpp \
 	expr_manager.cpp \
 	node_value.cpp \
-	expr.cpp
+	expr.cpp \
+	command.h \
+	command.cpp
 
+EXTRA_DIST = @srcdir@/kind.h kind_prologue.h kind_middle.h kind_epilogue.h
+
+@srcdir@/kind.h: @srcdir@/mkkind kind_prologue.h kind_middle.h kind_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+	chmod +x @srcdir@/mkkind
+	(@srcdir@/mkkind \
+		@srcdir@/kind_prologue.h \
+		@srcdir@/kind_middle.h \
+		@srcdir@/kind_epilogue.h \
+		`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+	> @srcdir@/kind.h) || (rm -f @srcdir@/kind.h && exit 1)
+
+BUILT_SOURCES = @srcdir@/kind.h
+dist-hook: @srcdir@/kind.h
+MAINTAINERCLEANFILES = @srcdir@/kind.h
diff --git a/src/util/command.cpp b/src/expr/command.cpp
index 58f8b41bb..2f8dd789e 100644
--- a/src/util/command.cpp
+++ b/src/expr/command.cpp
@@ -13,7 +13,7 @@
  ** Implementation of command objects.
  **/
 
-#include "util/command.h"
+#include "expr/command.h"
 #include "smt/smt_engine.h"
 
 using namespace std;
diff --git a/src/util/command.h b/src/expr/command.h
index 81af801d1..dedefb782 100644
--- a/src/util/command.h
+++ b/src/expr/command.h
@@ -72,7 +72,6 @@ protected:
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
 public:
-  CheckSatCommand();
   CheckSatCommand(const BoolExpr& e);
   void invoke(SmtEngine* smt);
   Result getResult();
@@ -198,9 +197,6 @@ inline void AssertCommand::toStream(std::ostream& out) const {
 
 /* class CheckSatCommand */
 
-inline CheckSatCommand::CheckSatCommand() {
-}
-
 inline CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
   d_expr(e) {
 }
diff --git a/src/expr/kind.h b/src/expr/kind.h
deleted file mode 100644
index 575a4790c..000000000
--- a/src/expr/kind.h
+++ /dev/null
@@ -1,100 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** kind.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): cconway, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** Kinds of Nodes.
- **/
-
-#ifndef __CVC4__KIND_H
-#define __CVC4__KIND_H
-
-#include "cvc4_config.h"
-#include <iostream>
-
-namespace CVC4 {
-
-// TODO: create this file (?) from theory solver headers so that we
-// have a collection of kinds from all.  This file is mainly a
-// placeholder for design & development work.
-
-enum Kind {
-  /* undefined */
-  UNDEFINED_KIND = -1,
-  /** Null Kind */
-  NULL_EXPR,
-
-  /* built-ins */
-  EQUAL,
-  ITE,
-  SKOLEM,
-  VARIABLE,
-  APPLY,
-
-  /* propositional connectives */
-  FALSE,
-  TRUE,
-
-  NOT,
-
-  AND,
-  IFF,
-  IMPLIES,
-  OR,
-  XOR,
-
-  /* from arith */
-  PLUS,
-  MINUS,
-  MULT
-};/* enum Kind */
-
-inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
-  using namespace CVC4;
-
-  switch(k) {
-
-  /* special cases */
-  case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
-  case NULL_EXPR:      out << "NULL";           break;
-
-  case EQUAL:          out << "EQUAL";          break;
-  case ITE:            out << "ITE";            break;
-  case SKOLEM:         out << "SKOLEM";         break;
-  case VARIABLE:       out << "VARIABLE";       break;
-  case APPLY:          out << "APPLY";          break;
-
-  /* propositional connectives */
-  case FALSE:          out << "FALSE";          break;
-  case TRUE:           out << "TRUE";           break;
-
-  case NOT:            out << "NOT";            break;
-
-  case AND:            out << "AND";            break;
-  case IFF:            out << "IFF";            break;
-  case IMPLIES:        out << "IMPLIES";        break;
-  case OR:             out << "OR";             break;
-  case XOR:            out << "XOR";            break;
-
-  /* from arith */
-  case PLUS:           out << "PLUS";           break;
-  case MINUS:          out << "MINUS";          break;
-  case MULT:           out << "MULT";           break;
-
-  default:             out << "UNKNOWNKIND!" << int(k); break;
-  }
-
-  return out;
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__KIND_H */
diff --git a/src/expr/kind_epilogue.h b/src/expr/kind_epilogue.h
new file mode 100644
index 000000000..0db7038d8
--- /dev/null
+++ b/src/expr/kind_epilogue.h
@@ -0,0 +1,25 @@
+/*********************                                           -*- C++ -*-  */
+/** kind_epilogue.h
+ ** Original author: 
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Kinds of Nodes.
+ **/
+
+  case LAST_KIND: out << "LAST_KIND"; break;
+  default: out << "UNKNOWNKIND!" << int(k); break;
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__KIND_H */
diff --git a/src/expr/kind_middle.h b/src/expr/kind_middle.h
new file mode 100644
index 000000000..6c352c3c9
--- /dev/null
+++ b/src/expr/kind_middle.h
@@ -0,0 +1,33 @@
+/*********************                                           -*- C++ -*-  */
+/** kind_middle.h
+ ** Original author: 
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Kinds of Nodes.
+ **/
+
+  LAST_KIND
+
+};/* enum Kind */
+
+inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
+  using namespace CVC4;
+
+  switch(k) {
+
+  /* special cases */
+  case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
+  case NULL_EXPR: out << "NULL"; break;
+
+  case EQUAL: out << "EQUAL"; break;
+  case ITE: out << "ITE"; break;
+  case SKOLEM: out << "SKOLEM"; break;
+  case VARIABLE: out << "VARIABLE"; break;
diff --git a/src/expr/kind_prologue.h b/src/expr/kind_prologue.h
new file mode 100644
index 000000000..cf9d2e3be
--- /dev/null
+++ b/src/expr/kind_prologue.h
@@ -0,0 +1,34 @@
+/*********************                                           -*- C++ -*-  */
+/** kind_prologue.h
+ ** Original author: 
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Kinds of Nodes.
+ **/
+
+#ifndef __CVC4__KIND_H
+#define __CVC4__KIND_H
+
+#include "cvc4_config.h"
+#include <iostream>
+
+namespace CVC4 {
+
+enum Kind {
+  /* undefined */
+  UNDEFINED_KIND = -1,
+  /** Null Kind */
+  NULL_EXPR,
+
+  /* built-ins */
+  EQUAL,
+  ITE,
+  SKOLEM,
+  VARIABLE,
diff --git a/src/expr/mkkind b/src/expr/mkkind
new file mode 100755
index 000000000..c8ad61571
--- /dev/null
+++ b/src/expr/mkkind
@@ -0,0 +1,54 @@
+#!/bin/bash
+#
+# mkkind
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+#
+# The purpose of this script is to create kind.h from a prologue,
+# middle, epilogue, and a list of theory kinds.
+#
+# Invocation:
+#
+#   mkkind prologue-file middle-file epilogue-file theory-kind-files...
+#
+# Output is to standard out.
+#
+
+cat <<EOF
+/*********************                                           -*- C++ -*-  */
+/** kind.h
+ **
+ ** Copyright 2009, 2010  The AcSys Group, New York University, and as below.
+ **
+ ** This header file automatically generated by:
+ **
+ **     $0 $@
+ **
+ ** for the CVC4 project.
+ **
+ **/
+
+EOF
+
+prologue=$1; shift
+middle=$1; shift
+epilogue=$1; shift
+
+cases=
+cat "$prologue"
+while [ $# -gt 0 ]; do
+  b=$(basename $(dirname "$1"))
+  echo
+  echo "  /* from $b */"
+  cases="$cases
+  /* from $b */
+"
+  for r in `cat "$1"`; do
+    echo "  $r,"
+    cases="$cases  case $r: out << \"$r\"; break;
+"
+  done
+  shift
+done
+cat "$middle"
+echo "$cases"
+cat "$epilogue"
diff --git a/src/main/about.h b/src/main/about.h
index d00b1eaec..a30cffd39 100644
--- a/src/main/about.h
+++ b/src/main/about.h
@@ -21,9 +21,11 @@ namespace main {
 
 const char about[] = "\
 This is a pre-release of CVC4.\n\
-Copyright (C) 2009 The ACSys Group\n\
-                   Courant Institute of Mathematical Sciences,\n\
-                   New York University\n\
+Copyright (C) 2009, 2010\n\
+  The ACSys Group\n\
+  Courant Institute of Mathematical Sciences,\n\
+  New York University\n\
+  New York, NY  10012  USA\n\
 ";
 
 }/* CVC4::main namespace */
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 6eb70a3e1..f4d32cd68 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -56,25 +56,35 @@ CNF conversions currently supported as arguments to the --cnf option:\n\
 enum OptionValue {
   CNF = 256, /* no clash with char options */
   SMTCOMP,
-  STATS
+  STATS,
+  SEGV_NOSPIN
 };/* enum OptionValue */
 
 // FIXME add a comment here describing the option array
 static struct option cmdlineOptions[] = {
   // name, has_arg, *flag, val
-  { "help"   , no_argument      , NULL, 'h'     },
-  { "version", no_argument      , NULL, 'V'     },
-  { "verbose", no_argument      , NULL, 'v'     },
-  { "quiet"  , no_argument      , NULL, 'q'     },
-  { "lang"   , required_argument, NULL, 'L'     },
-  { "debug"  , required_argument, NULL, 'd'     },
-  { "cnf"    , required_argument, NULL, CNF     },
-  { "smtcomp", no_argument      , NULL, SMTCOMP },
-  { "stats"  , no_argument      , NULL, STATS   }
+  { "help"       , no_argument      , NULL, 'h'         },
+  { "version"    , no_argument      , NULL, 'V'         },
+  { "verbose"    , no_argument      , NULL, 'v'         },
+  { "quiet"      , no_argument      , NULL, 'q'         },
+  { "lang"       , required_argument, NULL, 'L'         },
+  { "debug"      , required_argument, NULL, 'd'         },
+  { "cnf"        , required_argument, NULL, CNF         },
+  { "smtcomp"    , no_argument      , NULL, SMTCOMP     },
+  { "stats"      , no_argument      , NULL, STATS       },
+  { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN }
 };/* if you add things to the above, please remember to update usage.h! */
 
-int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionException) {
-  const char *progName = argv[0];
+/** Full argv[0] */
+const char *progPath;
+
+/** Just the basename component of argv[0] */
+const char *progName;
+
+/** Parse argc/argv and put the result into a CVC4::Options struct. */
+int parseOptions(int argc, char** argv, CVC4::Options* opts)
+throw(OptionException) {
+  progPath = progName = argv[0];
   int c;
 
   // find the base name of the program
@@ -85,17 +95,18 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
   opts->binary_name = string(progName);
 
   // FIXME add a comment here describing the option string
-  while((c = getopt_long(argc, argv, "+:hVvqL:d:", cmdlineOptions, NULL)) != -1) {
+  while((c = getopt_long(argc, argv,
+                         "+:hVvqL:d:",
+                         cmdlineOptions, NULL)) != -1) {
     switch(c) {
 
     case 'h':
       printf(usage, opts->binary_name.c_str());
       exit(1);
-      break;
 
     case 'V':
       fputs(about, stdout);
-      break;
+      exit(0);
 
     case 'v':
       ++opts->verbosity;
@@ -148,6 +159,10 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
       opts->statistics = true;
       break;
 
+    case SEGV_NOSPIN:
+      segvNoSpin = true;
+      break;
+
     case SMTCOMP:
       // silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input)
       opts->smtcomp_mode = true;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 02ebe8deb..de179edb8 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -25,7 +25,7 @@
 #include "parser/parser.h"
 #include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
-#include "util/command.h"
+#include "expr/command.h"
 #include "util/result.h"
 #include "util/Assert.h"
 #include "util/output.h"
diff --git a/src/main/main.h b/src/main/main.h
index 9b2f4fcbe..0c78912ae 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -28,12 +28,31 @@ struct Options;
 
 namespace main {
 
+/** Class representing an option-parsing exception. */
 class OptionException : public CVC4::Exception {
 public:
-  OptionException(const std::string& s) throw() : CVC4::Exception("Error in option parsing: " + s) {}
+  OptionException(const std::string& s) throw() :
+    CVC4::Exception("Error in option parsing: " + s) {
+  }
 };/* class OptionException */
 
+/** Full argv[0] */
+extern const char *progPath;
+
+/** Just the basename component of argv[0] */
+extern const char *progName;
+
+/**
+ * If true, will not spin on segfault even when CVC4_DEBUG is on.
+ * Useful for nightly regressions, noninteractive performance runs
+ * etc.  See util.cpp.
+ */
+extern bool segvNoSpin;
+
+/** Parse argc/argv and put the result into a CVC4::Options struct. */
 int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException);
+
+/** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw();
 
 }/* CVC4::main namespace */
diff --git a/src/main/usage.h b/src/main/usage.h
index f6c089f1d..6927f0f2f 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -27,8 +27,7 @@ usage: %s [options] [input-file]\n\
 Without an input file, or with `-', CVC4 reads from standard input.\n\
 \n\
 CVC4 options:\n\
-   --lang | -L     set input language (--lang help gives a list;\n\
-                                       `auto' is default)\n\
+   --lang | -L     force input language (default is `auto'; see --lang help)\n\
    --version | -V  identify this CVC4 binary\n\
    --help | -h     this command line reference\n\
    --verbose | -v  increase verbosity (repeatable)\n\
@@ -36,6 +35,7 @@ CVC4 options:\n\
    --debug | -d    debugging for something (e.g. --debug arith)\n\
    --smtcomp       competition mode (very quiet)\n\
    --stats         give statistics on exit\n\
+   --segv-nospin   (debug builds only) don't spin on segfault waiting for gdb\n\
 ";
 
 }/* CVC4::main namespace */
diff --git a/src/main/util.cpp b/src/main/util.cpp
index df4ab803d..03ae26092 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -10,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** [[ Add file-specific comments here ]]
+ ** Utilities for the main driver.
  **/
 
 #include <cstdio>
@@ -22,24 +22,48 @@
 #include "util/exception.h"
 #include "config.h"
 
+#include "main.h"
+
 using CVC4::Exception;
 using namespace std;
 
 namespace CVC4 {
 namespace main {
 
-// FIXME add comments to functions
+/**
+ * If true, will not spin on segfault even when CVC4_DEBUG is on.
+ * Useful for nightly regressions, noninteractive performance runs
+ * etc.
+ */
+bool segvNoSpin = false;
 
+/** Handler for SIGINT, i.e., when the user hits control C. */
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
   abort();
 }
 
+/** Handler for SIGSEGV (segfault). */
 void segv_handler(int sig, siginfo_t* info, void*) {
+#ifdef CVC4_DEBUG
+  fprintf(stderr, "CVC4 suffered a segfault in DEBUG mode.\n");
+  if(segvNoSpin) {
+    fprintf(stderr, "No-spin requested, aborting...\n");
+    abort();
+  } else {
+    fprintf(stderr, "Spinning so that a debugger can be connected.\n");
+    fprintf(stderr, "Try:  gdb %s %u\n", progName, getpid());
+    for(;;) {
+      sleep(60);
+    }
+  }
+#else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 suffered a segfault.\n");
   abort();
+#endif /* CVC4_DEBUG */
 }
 
+/** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw() {
   struct sigaction act1;
   act1.sa_sigaction = sigint_handler;
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 053eb8a11..58f1babd0 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -25,7 +25,7 @@
 #include "antlr_parser.h"
 #include "util/output.h"
 #include "util/Assert.h"
-#include "util/command.h"
+#include "expr/command.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 5832847fc..9a77ea178 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -10,13 +10,12 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- **
  ** Parser for CVC presentation language.
  **/
 
 header "post_include_hpp" {
 #include "parser/antlr_parser.h"
-#include "util/command.h"
+#include "expr/command.h"
 }
 
 header "post_include_cpp" {
@@ -74,7 +73,7 @@ command returns [CVC4::Command* cmd = 0]
   : ASSERT   f = formula  SEMICOLON { cmd = new AssertCommand(f);   }
   | QUERY    f = formula  SEMICOLON { cmd = new QueryCommand(f);    }
   | CHECKSAT f = formula  SEMICOLON { cmd = new CheckSatCommand(f); }
-  | CHECKSAT              SEMICOLON { cmd = new CheckSatCommand();  }
+  | CHECKSAT              SEMICOLON { cmd = new CheckSatCommand(getTrueExpr()); }
   | identifierList[ids, CHECK_UNDECLARED] COLON type {
       // FIXME: switch on type (may not be predicates)
       vector<string> sorts;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 6a70b5181..71f38e87f 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -18,7 +18,7 @@
 #include <antlr/CharScanner.hpp>
 
 #include "parser.h"
-#include "util/command.h"
+#include "expr/command.h"
 #include "util/output.h"
 #include "util/Assert.h"
 #include "parser_exception.h"
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index fe98063cc..8bc557bbd 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -15,7 +15,7 @@
 
 header "post_include_hpp" {
 #include "parser/antlr_parser.h"
-#include "util/command.h"
+#include "expr/command.h"
 }
 
 header "post_include_cpp" {
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 047daace8..f4b10414c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -109,7 +109,7 @@ Result PropEngine::solve() {
     d_restartMayBeNeeded = true;
   }
 
-  Message() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
+  Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
   
   if(result){
     for(map<Node,Lit>::iterator atomIter = d_atom2lit.begin();
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2d36da0f1..09790882c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -14,7 +14,7 @@
 
 #include "smt/smt_engine.h"
 #include "util/exception.h"
-#include "util/command.h"
+#include "expr/command.h"
 #include "util/output.h"
 #include "expr/node_builder.h"
 #include "util/options.h"
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 316c747de..9c3431499 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -10,8 +10,6 @@ libutil_la_SOURCES = \
 	Assert.cpp \
 	Makefile.am \
 	Makefile.in \
-	command.cpp \
-	command.h \
 	debug.h \
 	decision_engine.cpp \
 	decision_engine.h \
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 1d5de423e..28a38892f 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -20,7 +20,7 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "parser/parser.h"
-#include "util/command.h"
+#include "expr/command.h"
 
 using namespace CVC4;
 using namespace CVC4::parser;