merge from symmetry branch

27 files changed, 1665 insertions, 159 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 8d6748e54..2783e8eaa 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -27,21 +27,26 @@
 #include "smt/bad_option_exception.h"
 #include "util/output.h"
 #include "util/sexpr.h"
+#include "expr/node.h"
+#include "printer/printer.h"
 
 using namespace std;
 
 namespace CVC4 {
 
 std::ostream& operator<<(std::ostream& out, const Command& c) {
-  c.toStream(out);
+  c.toStream(out,
+             Node::setdepth::getDepth(out),
+             Node::printtypes::getPrintTypes(out),
+             Node::setlanguage::getLanguage(out));
   return out;
 }
 
-ostream& operator<<(ostream& out, const Command* command) {
-  if(command == NULL) {
+ostream& operator<<(ostream& out, const Command* c) {
+  if(c == NULL) {
     out << "null";
   } else {
-    command->toStream(out);
+    out << *c;
   }
   return out;
 }
@@ -59,6 +64,11 @@ std::string Command::toString() const {
   return ss.str();
 }
 
+void Command::toStream(std::ostream& out, int toDepth, bool types,
+                       OutputLanguage language) const {
+  Printer::getPrinter(language)->toStream(out, this, toDepth, types);
+}
+
 void Command::printResult(std::ostream& out) const {
 }
 
@@ -72,10 +82,6 @@ void EmptyCommand::invoke(SmtEngine* smtEngine) {
   /* empty commands have no implementation */
 }
 
-void EmptyCommand::toStream(std::ostream& out) const {
-  out << "EmptyCommand(" << d_name << ")";
-}
-
 /* class AssertCommand */
 
 AssertCommand::AssertCommand(const BoolExpr& e) :
@@ -86,30 +92,18 @@ void AssertCommand::invoke(SmtEngine* smtEngine) {
   smtEngine->assertFormula(d_expr);
 }
 
-void AssertCommand::toStream(std::ostream& out) const {
-  out << "Assert(" << d_expr << ")";
-}
-
 /* class PushCommand */
 
 void PushCommand::invoke(SmtEngine* smtEngine) {
   smtEngine->push();
 }
 
-void PushCommand::toStream(std::ostream& out) const {
-  out << "Push()";
-}
-
 /* class PopCommand */
 
 void PopCommand::invoke(SmtEngine* smtEngine) {
   smtEngine->pop();
 }
 
-void PopCommand::toStream(std::ostream& out) const {
-  out << "Pop()";
-}
-
 /* class CheckSatCommand */
 
 CheckSatCommand::CheckSatCommand(const BoolExpr& expr) :
@@ -120,14 +114,6 @@ void CheckSatCommand::invoke(SmtEngine* smtEngine) {
   d_result = smtEngine->checkSat(d_expr);
 }
 
-void CheckSatCommand::toStream(std::ostream& out) const {
-  if(d_expr.isNull()) {
-    out << "CheckSat()";
-  } else {
-    out << "CheckSat(" << d_expr << ")";
-  }
-}
-
 Result CheckSatCommand::getResult() const {
   return d_result;
 }
@@ -154,19 +140,11 @@ void QueryCommand::printResult(std::ostream& out) const {
   out << d_result << endl;
 }
 
-void QueryCommand::toStream(std::ostream& out) const {
-  out << "Query(" << d_expr << ')';
-}
-
 /* class QuitCommand */
 
 QuitCommand::QuitCommand() {
 }
 
-void QuitCommand::toStream(std::ostream& out) const {
-  out << "Quit()" << endl;
-}
-
 /* class CommandSequence */
 
 CommandSequence::CommandSequence() :
@@ -197,14 +175,6 @@ void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
   }
 }
 
-void CommandSequence::toStream(std::ostream& out) const {
-  out << "CommandSequence[" << endl;
-  for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
-    out << *d_commandSequence[i] << endl;
-  }
-  out << "]";
-}
-
 /* class DeclarationCommand */
 
 DeclarationCommand::DeclarationCommand(const std::string& id, Type t) :
@@ -225,14 +195,6 @@ Type DeclarationCommand::getDeclaredType() const {
   return d_type;
 }
 
-void DeclarationCommand::toStream(std::ostream& out) const {
-  out << "Declare([";
-  copy( d_declaredSymbols.begin(), d_declaredSymbols.end() - 1,
-        ostream_iterator<string>(out, ", ") );
-  out << d_declaredSymbols.back();
-  out << "])";
-}
-
 /* class DefineFunctionCommand */
 
 DefineFunctionCommand::DefineFunctionCommand(Expr func,
@@ -247,16 +209,6 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
   smtEngine->defineFunction(d_func, d_formals, d_formula);
 }
 
-void DefineFunctionCommand::toStream(std::ostream& out) const {
-  out << "DefineFunction( \"" << d_func << "\", [";
-  if(d_formals.size() > 0) {
-    copy( d_formals.begin(), d_formals.end() - 1,
-          ostream_iterator<Expr>(out, ", ") );
-    out << d_formals.back();
-  }
-  out << "], << " << d_formula << " >> )";
-}
-
 /* class DefineFunctionCommand */
 
 DefineNamedFunctionCommand::DefineNamedFunctionCommand(Expr func,
@@ -273,12 +225,6 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) {
   }
 }
 
-void DefineNamedFunctionCommand::toStream(std::ostream& out) const {
-  out << "DefineNamedFunction( ";
-  this->DefineFunctionCommand::toStream(out);
-  out << " )";
-}
-
 /* class Simplify */
 
 SimplifyCommand::SimplifyCommand(Expr term) :
@@ -286,7 +232,7 @@ SimplifyCommand::SimplifyCommand(Expr term) :
 }
 
 void SimplifyCommand::invoke(SmtEngine* smtEngine) {
-#warning TODO: what is this
+  d_result = smtEngine->simplify(d_term);
 }
 
 Expr SimplifyCommand::getResult() const {
@@ -297,10 +243,6 @@ void SimplifyCommand::printResult(std::ostream& out) const {
   out << d_result << endl;
 }
 
-void SimplifyCommand::toStream(std::ostream& out) const {
-  out << "Simplify( << " << d_term << " >> )";
-}
-
 /* class GetValueCommand */
 
 GetValueCommand::GetValueCommand(Expr term) :
@@ -320,10 +262,6 @@ void GetValueCommand::printResult(std::ostream& out) const {
   out << d_result << endl;
 }
 
-void GetValueCommand::toStream(std::ostream& out) const {
-  out << "GetValue( << " << d_term << " >> )";
-}
-
 /* class GetAssignmentCommand */
 
 GetAssignmentCommand::GetAssignmentCommand() {
@@ -341,10 +279,6 @@ void GetAssignmentCommand::printResult(std::ostream& out) const {
   out << d_result << endl;
 }
 
-void GetAssignmentCommand::toStream(std::ostream& out) const {
-  out << "GetAssignment()";
-}
-
 /* class GetAssertionsCommand */
 
 GetAssertionsCommand::GetAssertionsCommand() {
@@ -365,10 +299,6 @@ void GetAssertionsCommand::printResult(std::ostream& out) const {
   out << d_result;
 }
 
-void GetAssertionsCommand::toStream(std::ostream& out) const {
-  out << "GetAssertions()";
-}
-
 /* class SetBenchmarkStatusCommand */
 
 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
@@ -390,10 +320,6 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
   }
 }
 
-void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
-  out << "SetBenchmarkStatus(" << d_status << ")";
-}
-
 /* class SetBenchmarkLogicCommand */
 
 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) :
@@ -409,10 +335,6 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
   }
 }
 
-void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
-  out << "SetBenchmarkLogic(" << d_logic << ")";
-}
-
 /* class SetInfoCommand */
 
 SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) :
@@ -441,10 +363,6 @@ void SetInfoCommand::printResult(std::ostream& out) const {
   }
 }
 
-void SetInfoCommand::toStream(std::ostream& out) const {
-  out << "SetInfo(" << d_flag << ", " << d_sexpr << ")";
-}
-
 /* class GetInfoCommand */
 
 GetInfoCommand::GetInfoCommand(std::string flag) :
@@ -471,10 +389,6 @@ void GetInfoCommand::printResult(std::ostream& out) const {
   }
 }
 
-void GetInfoCommand::toStream(std::ostream& out) const {
-  out << "GetInfo(" << d_flag << ")";
-}
-
 /* class SetOptionCommand */
 
 SetOptionCommand::SetOptionCommand(std::string flag, SExpr& sexpr) :
@@ -503,10 +417,6 @@ void SetOptionCommand::printResult(std::ostream& out) const {
   }
 }
 
-void SetOptionCommand::toStream(std::ostream& out) const {
-  out << "SetOption(" << d_flag << ", " << d_sexpr << ")";
-}
-
 /* class GetOptionCommand */
 
 GetOptionCommand::GetOptionCommand(std::string flag) :
@@ -531,10 +441,6 @@ void GetOptionCommand::printResult(std::ostream& out) const {
   }
 }
 
-void GetOptionCommand::toStream(std::ostream& out) const {
-  out << "GetOption(" << d_flag << ")";
-}
-
 /* class DatatypeDeclarationCommand */
 
 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) :
@@ -553,17 +459,6 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
   //smtEngine->addDatatypeDefinitions(d_datatype);
 }
 
-void DatatypeDeclarationCommand::toStream(std::ostream& out) const {
-  out << "DatatypeDeclarationCommand([";
-  for(vector<DatatypeType>::const_iterator i = d_datatypes.begin(),
-        i_end = d_datatypes.end();
-      i != i_end;
-      ++i) {
-    out << *i << ";" << endl;
-  }
-  out << "])";
-}
-
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out,
                          BenchmarkStatus status) {
diff --git a/src/expr/command.h b/src/expr/command.h
index d0b72c3dd..50d382038 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -62,7 +62,8 @@ public:
   virtual void invoke(SmtEngine* smtEngine) = 0;
   virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
   virtual ~Command() {};
-  virtual void toStream(std::ostream&) const = 0;
+  virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+                        OutputLanguage language = language::output::LANG_AST) const;
   std::string toString() const;
   virtual void printResult(std::ostream& out) const;
 };/* class Command */
@@ -77,7 +78,7 @@ protected:
 public:
   EmptyCommand(std::string name = "");
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getName() const { return d_name; }
 };/* class EmptyCommand */
 
 class CVC4_PUBLIC AssertCommand : public Command {
@@ -86,19 +87,17 @@ protected:
 public:
   AssertCommand(const BoolExpr& e);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  BoolExpr getExpr() const { return d_expr; }
 };/* class AssertCommand */
 
 class CVC4_PUBLIC PushCommand : public Command {
 public:
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
 };/* class PushCommand */
 
 class CVC4_PUBLIC PopCommand : public Command {
 public:
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
 };/* class PopCommand */
 
 class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
@@ -110,7 +109,6 @@ public:
   DeclarationCommand(const std::vector<std::string>& ids, Type t);
   const std::vector<std::string>& getDeclaredSymbols() const;
   Type getDeclaredType() const;
-  void toStream(std::ostream& out) const;
 };/* class DeclarationCommand */
 
 class CVC4_PUBLIC DefineFunctionCommand : public Command {
@@ -123,7 +121,9 @@ public:
                         const std::vector<Expr>& formals,
                         Expr formula);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  Expr getFunction() const { return d_func; }
+  const std::vector<Expr>& getFormals() const { return d_formals; }
+  Expr getFormula() const { return d_formula; }
 };/* class DefineFunctionCommand */
 
 /**
@@ -137,7 +137,6 @@ public:
                              const std::vector<Expr>& formals,
                              Expr formula);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
 };/* class DefineNamedFunctionCommand */
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
@@ -147,9 +146,9 @@ protected:
 public:
   CheckSatCommand(const BoolExpr& expr);
   void invoke(SmtEngine* smtEngine);
+  BoolExpr getExpr() const { return d_expr; }
   Result getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class CheckSatCommand */
 
 class CVC4_PUBLIC QueryCommand : public Command {
@@ -159,9 +158,9 @@ protected:
 public:
   QueryCommand(const BoolExpr& e);
   void invoke(SmtEngine* smtEngine);
+  BoolExpr getExpr() const { return d_expr; }
   Result getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class QueryCommand */
 
 // this is TRANSFORM in the CVC presentation language
@@ -172,9 +171,9 @@ protected:
 public:
   SimplifyCommand(Expr term);
   void invoke(SmtEngine* smtEngine);
+  Expr getTerm() const { return d_term; }
   Expr getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class SimplifyCommand */
 
 class CVC4_PUBLIC GetValueCommand : public Command {
@@ -184,9 +183,9 @@ protected:
 public:
   GetValueCommand(Expr term);
   void invoke(SmtEngine* smtEngine);
+  Expr getTerm() const { return d_term; }
   Expr getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class GetValueCommand */
 
 class CVC4_PUBLIC GetAssignmentCommand : public Command {
@@ -197,7 +196,6 @@ public:
   void invoke(SmtEngine* smtEngine);
   SExpr getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class GetAssignmentCommand */
 
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
@@ -208,7 +206,6 @@ public:
   void invoke(SmtEngine* smtEngine);
   std::string getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class GetAssertionsCommand */
 
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
@@ -218,7 +215,7 @@ protected:
 public:
   SetBenchmarkStatusCommand(BenchmarkStatus status);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  BenchmarkStatus getStatus() const { return d_status; }
 };/* class SetBenchmarkStatusCommand */
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
@@ -228,7 +225,7 @@ protected:
 public:
   SetBenchmarkLogicCommand(std::string logic);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getLogic() const { return d_logic; }
 };/* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC SetInfoCommand : public Command {
@@ -239,7 +236,8 @@ protected:
 public:
   SetInfoCommand(std::string flag, SExpr& sexpr);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getFlag() const { return d_flag; }
+  SExpr getSExpr() const { return d_sexpr; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class SetInfoCommand */
@@ -251,7 +249,7 @@ protected:
 public:
   GetInfoCommand(std::string flag);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getFlag() const { return d_flag; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class GetInfoCommand */
@@ -264,7 +262,8 @@ protected:
 public:
   SetOptionCommand(std::string flag, SExpr& sexpr);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getFlag() const { return d_flag; }
+  SExpr getSExpr() const { return d_sexpr; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class SetOptionCommand */
@@ -276,7 +275,7 @@ protected:
 public:
   GetOptionCommand(std::string flag);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getFlag() const { return d_flag; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class GetOptionCommand */
@@ -288,13 +287,12 @@ public:
   DatatypeDeclarationCommand(const DatatypeType& datatype);
   DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  const std::vector<DatatypeType>& getDatatypes() const { return d_datatypes; }
 };/* class DatatypeDeclarationCommand */
 
 class CVC4_PUBLIC QuitCommand : public EmptyCommand {
 public:
   QuitCommand();
-  void toStream(std::ostream& out) const;
 };/* class QuitCommand */
 
 class CVC4_PUBLIC CommandSequence : public Command {
@@ -309,7 +307,6 @@ public:
   void invoke(SmtEngine* smtEngine);
   void invoke(SmtEngine* smtEngine, std::ostream& out);
   void addCommand(Command* cmd);
-  void toStream(std::ostream& out) const;
 
   typedef std::vector<Command*>::iterator iterator;
   typedef std::vector<Command*>::const_iterator const_iterator;
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 6cdf878a0..5863ded9f 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -17,10 +17,15 @@
  **/
 
 #include "printer/ast/ast_printer.h"
+#include "expr/expr.h" // for ExprSetDepth etc..
 #include "util/language.h" // for LANG_AST
 #include "expr/node_manager.h" // for VarNameAttr
+#include "expr/command.h"
 
 #include <iostream>
+#include <vector>
+#include <string>
+#include <typeinfo>
 
 using namespace std;
 
@@ -29,7 +34,7 @@ namespace printer {
 namespace ast {
 
 void AstPrinter::toStream(std::ostream& out, TNode n,
-                                   int toDepth, bool types) const {
+                          int toDepth, bool types) const {
   // null
   if(n.getKind() == kind::NULL_EXPR) {
     out << "null";
@@ -92,6 +97,170 @@ void AstPrinter::toStream(std::ostream& out, TNode n,
   out << ')';
 }/* AstPrinter::toStream() */
 
+template <class T>
+static bool tryToStream(std::ostream& out, const Command* c);
+
+void AstPrinter::toStream(std::ostream& out, const Command* c,
+                          int toDepth, bool types) const {
+  expr::ExprSetDepth::Scope sdScope(out, toDepth);
+  expr::ExprPrintTypes::Scope ptScope(out, types);
+
+  if(tryToStream<EmptyCommand>(out, c) ||
+     tryToStream<AssertCommand>(out, c) ||
+     tryToStream<PushCommand>(out, c) ||
+     tryToStream<PopCommand>(out, c) ||
+     tryToStream<CheckSatCommand>(out, c) ||
+     tryToStream<QueryCommand>(out, c) ||
+     tryToStream<QuitCommand>(out, c) ||
+     tryToStream<CommandSequence>(out, c) ||
+     tryToStream<DeclarationCommand>(out, c) ||
+     tryToStream<DefineFunctionCommand>(out, c) ||
+     tryToStream<DefineNamedFunctionCommand>(out, c) ||
+     tryToStream<SimplifyCommand>(out, c) ||
+     tryToStream<GetValueCommand>(out, c) ||
+     tryToStream<GetAssignmentCommand>(out, c) ||
+     tryToStream<GetAssertionsCommand>(out, c) ||
+     tryToStream<SetBenchmarkStatusCommand>(out, c) ||
+     tryToStream<SetBenchmarkLogicCommand>(out, c) ||
+     tryToStream<SetInfoCommand>(out, c) ||
+     tryToStream<GetInfoCommand>(out, c) ||
+     tryToStream<SetOptionCommand>(out, c) ||
+     tryToStream<GetOptionCommand>(out, c) ||
+     tryToStream<DatatypeDeclarationCommand>(out, c)) {
+    return;
+  }
+
+  Unhandled("don't know how to print a Command of class: %s", typeid(*c).name());
+
+}/* AstPrinter::toStream() */
+
+static void toStream(std::ostream& out, const EmptyCommand* c) {
+  out << "EmptyCommand(" << c->getName() << ")";
+}
+
+static void toStream(std::ostream& out, const AssertCommand* c) {
+  out << "Assert(" << c->getExpr() << ")";
+}
+
+static void toStream(std::ostream& out, const PushCommand* c) {
+  out << "Push()";
+}
+
+static void toStream(std::ostream& out, const PopCommand* c) {
+  out << "Pop()";
+}
+
+static void toStream(std::ostream& out, const CheckSatCommand* c) {
+  BoolExpr e = c->getExpr();
+  if(e.isNull()) {
+    out << "CheckSat()";
+  } else {
+    out << "CheckSat(" << e << ")";
+  }
+}
+
+static void toStream(std::ostream& out, const QueryCommand* c) {
+  out << "Query(" << c->getExpr() << ')';
+}
+
+static void toStream(std::ostream& out, const QuitCommand* c) {
+  out << "Quit()";
+}
+
+static void toStream(std::ostream& out, const CommandSequence* c) {
+  out << "CommandSequence[" << endl;
+  for(CommandSequence::const_iterator i = c->begin();
+      i != c->end();
+      ++i) {
+    out << *i << endl;
+  }
+  out << "]";
+}
+
+static void toStream(std::ostream& out, const DeclarationCommand* c) {
+  const vector<string>& declaredSymbols = c->getDeclaredSymbols();
+  out << "Declare([";
+  copy( declaredSymbols.begin(), declaredSymbols.end() - 1,
+        ostream_iterator<string>(out, ", ") );
+  out << declaredSymbols.back();
+  out << "])";
+}
+
+static void toStream(std::ostream& out, const DefineFunctionCommand* c) {
+  Expr func = c->getFunction();
+  const std::vector<Expr>& formals = c->getFormals();
+  Expr formula = c->getFormula();
+  out << "DefineFunction( \"" << func << "\", [";
+  if(formals.size() > 0) {
+    copy( formals.begin(), formals.end() - 1,
+          ostream_iterator<Expr>(out, ", ") );
+    out << formals.back();
+  }
+  out << "], << " << formula << " >> )";
+}
+
+static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) {
+  out << "DefineNamedFunction( ";
+  toStream(out, static_cast<const DefineFunctionCommand*>(c));
+  out << " )";
+}
+
+static void toStream(std::ostream& out, const SimplifyCommand* c) {
+  out << "Simplify( << " << c->getTerm() << " >> )";
+}
+
+static void toStream(std::ostream& out, const GetValueCommand* c) {
+  out << "GetValue( << " << c->getTerm() << " >> )";
+}
+
+static void toStream(std::ostream& out, const GetAssignmentCommand* c) {
+  out << "GetAssignment()";
+}
+static void toStream(std::ostream& out, const GetAssertionsCommand* c) {
+  out << "GetAssertions()";
+}
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) {
+  out << "SetBenchmarkStatus(" << c->getStatus() << ")";
+}
+static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) {
+  out << "SetBenchmarkLogic(" << c->getLogic() << ")";
+}
+static void toStream(std::ostream& out, const SetInfoCommand* c) {
+  out << "SetInfo(" << c->getFlag() << ", " << c->getSExpr() << ")";
+}
+
+static void toStream(std::ostream& out, const GetInfoCommand* c) {
+  out << "GetInfo(" << c->getFlag() << ")";
+}
+static void toStream(std::ostream& out, const SetOptionCommand* c) {
+  out << "SetOption(" << c->getFlag() << ", " << c->getSExpr() << ")";
+}
+
+static void toStream(std::ostream& out, const GetOptionCommand* c) {
+  out << "GetOption(" << c->getFlag() << ")";
+}
+
+static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) {
+  const vector<DatatypeType>& datatypes = c->getDatatypes();
+  out << "DatatypeDeclarationCommand([";
+  for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
+        i_end = datatypes.end();
+      i != i_end;
+      ++i) {
+    out << *i << ";" << endl;
+  }
+  out << "])";
+}
+
+template <class T>
+static bool tryToStream(std::ostream& out, const Command* c) {
+  if(typeid(*c) == typeid(T)) {
+    toStream(out, dynamic_cast<const T*>(c));
+    return true;
+  }
+  return false;
+}
+
 }/* CVC4::printer::ast namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index f3d927cfb..ddc3c50b8 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -32,6 +32,7 @@ namespace ast {
 class AstPrinter : public CVC4::Printer {
 public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const;
 };/* class AstPrinter */
 
 }/* CVC4::printer::ast namespace */
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index b2b801ded..11d633271 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -17,9 +17,15 @@
  **/
 
 #include "printer/cvc/cvc_printer.h"
-#include "util/language.h"
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "util/language.h" // for LANG_AST
+#include "expr/node_manager.h" // for VarNameAttr
+#include "expr/command.h"
 
 #include <iostream>
+#include <vector>
+#include <string>
+#include <typeinfo>
 #include <algorithm>
 #include <iterator>
 
@@ -324,7 +330,166 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
 
 }/* CvcPrinter::toStream() */
 
+template <class T>
+static bool tryToStream(std::ostream& out, const Command* c);
+
+void CvcPrinter::toStream(std::ostream& out, const Command* c,
+                           int toDepth, bool types) const {
+  expr::ExprSetDepth::Scope sdScope(out, toDepth);
+  expr::ExprPrintTypes::Scope ptScope(out, types);
+
+  if(tryToStream<AssertCommand>(out, c) ||
+     tryToStream<PushCommand>(out, c) ||
+     tryToStream<PopCommand>(out, c) ||
+     tryToStream<CheckSatCommand>(out, c) ||
+     tryToStream<QueryCommand>(out, c) ||
+     tryToStream<QuitCommand>(out, c) ||
+     tryToStream<CommandSequence>(out, c) ||
+     tryToStream<DeclarationCommand>(out, c) ||
+     tryToStream<DefineFunctionCommand>(out, c) ||
+     tryToStream<DefineNamedFunctionCommand>(out, c) ||
+     tryToStream<SimplifyCommand>(out, c) ||
+     tryToStream<GetValueCommand>(out, c) ||
+     tryToStream<GetAssignmentCommand>(out, c) ||
+     tryToStream<GetAssertionsCommand>(out, c) ||
+     tryToStream<SetBenchmarkStatusCommand>(out, c) ||
+     tryToStream<SetBenchmarkLogicCommand>(out, c) ||
+     tryToStream<SetInfoCommand>(out, c) ||
+     tryToStream<GetInfoCommand>(out, c) ||
+     tryToStream<SetOptionCommand>(out, c) ||
+     tryToStream<GetOptionCommand>(out, c) ||
+     tryToStream<DatatypeDeclarationCommand>(out, c)) {
+    return;
+  }
+
+  Unhandled("don't know how to print this command in CVC's presentation language: %s", c->toString().c_str());
+
+}/* CvcPrinter::toStream() */
+
+static void toStream(std::ostream& out, const AssertCommand* c) {
+  out << "ASSERT " << c->getExpr() << ";";
+}
+
+static void toStream(std::ostream& out, const PushCommand* c) {
+  out << "PUSH;";
+}
+
+static void toStream(std::ostream& out, const PopCommand* c) {
+  out << "POP;";
+}
+
+static void toStream(std::ostream& out, const CheckSatCommand* c) {
+  BoolExpr e = c->getExpr();
+  if(!e.isNull()) {
+    out << "CHECKSAT " << e << ";";
+  }
+  out << "CHECKSAT;";
+}
+
+static void toStream(std::ostream& out, const QueryCommand* c) {
+  out << "QUERY " << c->getExpr() << ";";
+}
+
+static void toStream(std::ostream& out, const QuitCommand* c) {
+  Unhandled("quit command");
+}
+
+static void toStream(std::ostream& out, const CommandSequence* c) {
+  for(CommandSequence::const_iterator i = c->begin();
+      i != c->end();
+      ++i) {
+    out << *i << endl;
+  }
+}
+
+static void toStream(std::ostream& out, const DeclarationCommand* c) {
+  const vector<string>& declaredSymbols = c->getDeclaredSymbols();
+  Type declaredType = c->getDeclaredType();
+  Assert(declaredSymbols.size() > 0);
+  copy( declaredSymbols.begin(), declaredSymbols.end() - 1,
+        ostream_iterator<string>(out, ", ") );
+  out << declaredSymbols.back();
+  out << " : " << declaredType << ";";
+}
+
+static void toStream(std::ostream& out, const DefineFunctionCommand* c) {
+  Expr func = c->getFunction();
+  const vector<Expr>& formals = c->getFormals();
+  Expr formula = c->getFormula();
+  out << func << " : " << func.getType() << " = LAMBDA(";
+  vector<Expr>::const_iterator i = formals.begin();
+  while(i != formals.end()) {
+    out << (*i) << ":" << (*i).getType();
+    if(++i != formals.end()) {
+      out << ", ";
+    }
+  }
+  out << "): " << formula << ";";
+}
+
+static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) {
+  toStream(out, static_cast<const DefineFunctionCommand*>(c));
+}
+
+static void toStream(std::ostream& out, const SimplifyCommand* c) {
+  out << "TRANSFORM " << c->getTerm() << ";";
+}
+
+static void toStream(std::ostream& out, const GetValueCommand* c) {
+  out << "% (get-value " << c->getTerm() << ")";
+}
+
+static void toStream(std::ostream& out, const GetAssignmentCommand* c) {
+  out << "% (get-assignment)";
+}
+
+static void toStream(std::ostream& out, const GetAssertionsCommand* c) {
+  out << "% (get-assertions)";
+}
+
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) {
+  out << "% (set-info :status " << c->getStatus() << ")";
+}
+
+static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) {
+  out << "% (set-logic " << c->getLogic() << ")";
+}
+
+static void toStream(std::ostream& out, const SetInfoCommand* c) {
+  out << "% (set-info " << c->getFlag() << " " << c->getSExpr() << ")";
+}
+
+static void toStream(std::ostream& out, const GetInfoCommand* c) {
+  out << "% (get-info " << c->getFlag() << ")";
+}
+
+static void toStream(std::ostream& out, const SetOptionCommand* c) {
+  out << "% (set-option " << c->getFlag() << " " << c->getSExpr() << ")";
+}
+
+static void toStream(std::ostream& out, const GetOptionCommand* c) {
+  out << "% (get-option " << c->getFlag() << ")";
+}
+
+static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) {
+  const vector<DatatypeType>& datatypes = c->getDatatypes();
+  for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
+        i_end = datatypes.end();
+      i != i_end;
+      ++i) {
+    out << *i;
+  }
+}
+
+template <class T>
+static bool tryToStream(std::ostream& out, const Command* c) {
+  if(typeid(*c) == typeid(T)) {
+    toStream(out, dynamic_cast<const T*>(c));
+    return true;
+  }
+  return false;
+}
+
 }/* CVC4::printer::cvc namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
-
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 410be0571..d794c82e8 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -32,6 +32,7 @@ namespace cvc {
 class CvcPrinter : public CVC4::Printer {
 public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const;
 };/* class CvcPrinter */
 
 }/* CVC4::printer::cvc namespace */
diff --git a/src/printer/printer.h b/src/printer/printer.h
index adbabe3c5..eae2fc48f 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -23,6 +23,7 @@
 
 #include "util/language.h"
 #include "expr/node.h"
+#include "expr/command.h"
 
 namespace CVC4 {
 
@@ -45,6 +46,10 @@ public:
   /** Write a Node out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, TNode n,
                         int toDepth, bool types) const = 0;
+
+  /** Write a Command out to a stream with this Printer. */
+  virtual void toStream(std::ostream& out, const Command* c,
+                        int toDepth, bool types) const = 0;
 };/* class Printer */
 
 }/* CVC4 namespace */
diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
index d03cfbbe0..de22a04c1 100644
--- a/src/printer/smt/smt_printer.cpp
+++ b/src/printer/smt/smt_printer.cpp
@@ -17,9 +17,15 @@
  **/
 
 #include "printer/smt/smt_printer.h"
-#include "util/language.h"
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "util/language.h" // for LANG_AST
+#include "expr/node_manager.h" // for VarNameAttr
+#include "expr/command.h"
 
 #include <iostream>
+#include <vector>
+#include <string>
+#include <typeinfo>
 
 using namespace std;
 
@@ -32,6 +38,11 @@ void SmtPrinter::toStream(std::ostream& out, TNode n,
   n.toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2);
 }/* SmtPrinter::toStream() */
 
+void SmtPrinter::toStream(std::ostream& out, const Command* c,
+                          int toDepth, bool types) const {
+  c->toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2);
+}/* SmtPrinter::toStream() */
+
 }/* CVC4::printer::smt namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h
index 8776b1308..058a6b18c 100644
--- a/src/printer/smt/smt_printer.h
+++ b/src/printer/smt/smt_printer.h
@@ -32,6 +32,7 @@ namespace smt {
 class SmtPrinter : public CVC4::Printer {
 public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const;
 };/* class SmtPrinter */
 
 }/* CVC4::printer::smt namespace */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0d5f367ad..5ce571904 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -19,6 +19,9 @@
 #include "printer/smt2/smt2_printer.h"
 
 #include <iostream>
+#include <vector>
+#include <string>
+#include <typeinfo>
 
 using namespace std;
 
@@ -235,6 +238,183 @@ void printBvParameterizedOp(std::ostream& out, TNode n) {
   out << ")";
 }
 
+template <class T>
+static bool tryToStream(std::ostream& out, const Command* c);
+
+void Smt2Printer::toStream(std::ostream& out, const Command* c,
+                           int toDepth, bool types) const {
+  expr::ExprSetDepth::Scope sdScope(out, toDepth);
+  expr::ExprPrintTypes::Scope ptScope(out, types);
+
+  if(tryToStream<AssertCommand>(out, c) ||
+     tryToStream<PushCommand>(out, c) ||
+     tryToStream<PopCommand>(out, c) ||
+     tryToStream<CheckSatCommand>(out, c) ||
+     tryToStream<QueryCommand>(out, c) ||
+     tryToStream<QuitCommand>(out, c) ||
+     tryToStream<CommandSequence>(out, c) ||
+     tryToStream<DeclarationCommand>(out, c) ||
+     tryToStream<DefineFunctionCommand>(out, c) ||
+     tryToStream<DefineNamedFunctionCommand>(out, c) ||
+     tryToStream<SimplifyCommand>(out, c) ||
+     tryToStream<GetValueCommand>(out, c) ||
+     tryToStream<GetAssignmentCommand>(out, c) ||
+     tryToStream<GetAssertionsCommand>(out, c) ||
+     tryToStream<SetBenchmarkStatusCommand>(out, c) ||
+     tryToStream<SetBenchmarkLogicCommand>(out, c) ||
+     tryToStream<SetInfoCommand>(out, c) ||
+     tryToStream<GetInfoCommand>(out, c) ||
+     tryToStream<SetOptionCommand>(out, c) ||
+     tryToStream<GetOptionCommand>(out, c) ||
+     tryToStream<DatatypeDeclarationCommand>(out, c)) {
+    return;
+  }
+
+  Unhandled("don't know how to print this command as SMT-LIBv2: %s", c->toString().c_str());
+
+}/* Smt2Printer::toStream() */
+
+static void toStream(std::ostream& out, const AssertCommand* c) {
+  out << "(assert " << c->getExpr() << ")";
+}
+
+static void toStream(std::ostream& out, const PushCommand* c) {
+  out << "(push 1)";
+}
+
+static void toStream(std::ostream& out, const PopCommand* c) {
+  out << "(pop 1)";
+}
+
+static void toStream(std::ostream& out, const CheckSatCommand* c) {
+  BoolExpr e = c->getExpr();
+  if(!e.isNull()) {
+    out << "(assert " << e << ")";
+  }
+  out << "(check-sat)";
+}
+
+static void toStream(std::ostream& out, const QueryCommand* c) {
+  Unhandled("query command");
+}
+
+static void toStream(std::ostream& out, const QuitCommand* c) {
+  out << "(exit)";
+}
+
+static void toStream(std::ostream& out, const CommandSequence* c) {
+  for(CommandSequence::const_iterator i = c->begin();
+      i != c->end();
+      ++i) {
+    out << *i << endl;
+  }
+}
+
+static void toStream(std::ostream& out, const DeclarationCommand* c) {
+  const vector<string>& declaredSymbols = c->getDeclaredSymbols();
+  Type declaredType = c->getDeclaredType();
+  for(vector<string>::const_iterator i = declaredSymbols.begin();
+      i != declaredSymbols.end();
+      ++i) {
+    if(declaredType.isFunction()) {
+      FunctionType ft = declaredType;
+      out << "(declare-fun " << *i << " (";
+      const vector<Type> argTypes = ft.getArgTypes();
+      if(argTypes.size() > 0) {
+        copy( argTypes.begin(), argTypes.end() - 1,
+              ostream_iterator<Type>(out, " ") );
+        out << argTypes.back();
+      }
+      out << ") " << ft.getRangeType() << ")";
+    } else {
+      out << "(declare-fun " << *i << " () " << declaredType << ")";
+    }
+  }
+}
+
+static void toStream(std::ostream& out, const DefineFunctionCommand* c) {
+  Expr func = c->getFunction();
+  const vector<Expr>& formals = c->getFormals();
+  Expr formula = c->getFormula();
+  out << "(define-fun " << func << " (";
+  for(vector<Expr>::const_iterator i = formals.begin();
+      i != formals.end();
+      ++i) {
+    out << "(" << (*i) << " " << (*i).getType() << ")";
+  }
+  out << ") " << FunctionType(func.getType()).getRangeType() << " " << formula << ")";
+}
+
+static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) {
+  out << "DefineNamedFunction( ";
+  toStream(out, static_cast<const DefineFunctionCommand*>(c));
+  out << " )";
+  Unhandled("define named function command");
+}
+
+static void toStream(std::ostream& out, const SimplifyCommand* c) {
+  out << "Simplify( << " << c->getTerm() << " >> )";
+  Unhandled("simplify command");
+}
+
+static void toStream(std::ostream& out, const GetValueCommand* c) {
+  out << "(get-value " << c->getTerm() << ")";
+}
+
+static void toStream(std::ostream& out, const GetAssignmentCommand* c) {
+  out << "(get-assignment)";
+}
+
+static void toStream(std::ostream& out, const GetAssertionsCommand* c) {
+  out << "(get-assertions)";
+}
+
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) {
+  out << "(set-info :status " << c->getStatus() << ")";
+}
+
+static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) {
+  out << "(set-logic " << c->getLogic() << ")";
+}
+
+static void toStream(std::ostream& out, const SetInfoCommand* c) {
+  out << "(set-info " << c->getFlag() << " " << c->getSExpr() << ")";
+}
+
+static void toStream(std::ostream& out, const GetInfoCommand* c) {
+  out << "(get-info " << c->getFlag() << ")";
+}
+
+static void toStream(std::ostream& out, const SetOptionCommand* c) {
+  out << "(set-option " << c->getFlag() << " " << c->getSExpr() << ")";
+}
+
+static void toStream(std::ostream& out, const GetOptionCommand* c) {
+  out << "(get-option " << c->getFlag() << ")";
+}
+
+static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) {
+  const vector<DatatypeType>& datatypes = c->getDatatypes();
+  out << "DatatypeDeclarationCommand([";
+  for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
+        i_end = datatypes.end();
+      i != i_end;
+      ++i) {
+    out << *i << ";" << endl;
+  }
+  out << "])";
+  Unhandled("datatype declaration command");
+}
+
+template <class T>
+static bool tryToStream(std::ostream& out, const Command* c) {
+  if(typeid(*c) == typeid(T)) {
+    toStream(out, dynamic_cast<const T*>(c));
+    return true;
+  }
+  return false;
+}
+
 }/* CVC4::printer::smt2 namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 6fce2dfff..4bae8a2e1 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -32,6 +32,7 @@ namespace smt2 {
 class Smt2Printer : public CVC4::Printer {
 public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const;
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 8e98f32c0..0c4f00875 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -240,8 +240,18 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
     if (ps.size() == 0)
         return ok = false;
     else if (ps.size() == 1){
-        assert(type != CLAUSE_LEMMA);
-        assert(value(ps[0]) == l_Undef);
+        if(in_solve) {
+          assert(type != CLAUSE_LEMMA);
+          assert(value(ps[0]) == l_Undef);
+        } else {
+          // [MGD] at "pre-solve" time we allow unit T-lemmas
+          if(value(ps[0]) == l_True) {
+            // this unit T-lemma is extraneous (perhaps it was
+            // discovered twice at presolve time)
+            return true;
+          }
+          assert(value(ps[0]) == l_Undef);
+        }
         uncheckedEnqueue(ps[0]);
         return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
     }else{
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index cbec9faea..4c9b66020 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -16,9 +16,9 @@
  ** Implementation of the propositional engine of CVC4.
  **/
 
-#include "cnf_stream.h"
-#include "prop_engine.h"
-#include "sat.h"
+#include "prop/cnf_stream.h"
+#include "prop/prop_engine.h"
+#include "prop/sat.h"
 
 #include "theory/theory_engine.h"
 #include "theory/registrar.h"
@@ -26,6 +26,8 @@
 #include "util/options.h"
 #include "util/output.h"
 #include "util/result.h"
+#include "expr/expr.h"
+#include "expr/command.h"
 
 #include <utility>
 #include <map>
@@ -88,6 +90,16 @@ void PropEngine::assertLemma(TNode node) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
+  if(Options::current()->preprocessOnly) {
+    if(Message.isOn()) {
+      // If "preprocess only" mode is in effect, the lemmas we get
+      // here are due to theory reasoning during preprocessing.  So
+      // push the lemma to the Message() stream.
+      expr::ExprSetDepth::Scope sdScope(Message.getStream(), -1);
+      Message() << AssertCommand(BoolExpr(node.toExpr())) << endl;
+    }
+  }
+
   //TODO This comment is now false
   // Assert as removable
   d_cnfStream->convertAndAssert(node, true, false);
@@ -124,6 +136,10 @@ Result PropEngine::checkSat() {
   // TODO This currently ignores conflicts (a dangerous practice).
   d_theoryEngine->presolve();
 
+  if(Options::current()->preprocessOnly) {
+    return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
+  }
+
   // Check the problem
   bool result = d_satSolver->solve();
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d85f28b23..fe5628dd0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -669,6 +669,18 @@ void SmtEnginePrivate::processAssertions() {
   // Simplify the assertions
   simplifyAssertions();
 
+  if(Options::current()->preprocessOnly) {
+    if(Message.isOn()) {
+      // Push the formula to the Message() stream
+      for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
+        expr::ExprSetDepth::Scope sdScope(Message.getStream(), -1);
+        Message() << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr())) << endl;
+      }
+    }
+    // We still call into SAT below so that we can output theory
+    // contributions that come from presolve().
+  }
+
   // Push the formula to SAT
   for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
     d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index fa885590b..4237e0992 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -286,6 +286,12 @@ Node TheoryEngine::getValue(TNode node) {
 }/* TheoryEngine::getValue(TNode node) */
 
 bool TheoryEngine::presolve() {
+  // NOTE that we don't look at d_theoryIsActive[] here.  First of
+  // all, we haven't done any pre-registration yet, so we don't know
+  // which theories are active.  Second, let's give each theory a shot
+  // at doing something with the input formula, even if it wouldn't
+  // otherwise be active.
+
   d_theoryOut.d_conflictNode = Node::null();
   d_theoryOut.d_propagatedLiterals.clear();
 
@@ -295,7 +301,7 @@ bool TheoryEngine::presolve() {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-    if (theory::TheoryTraits<THEORY>::hasPresolve && d_theoryIsActive[THEORY]) { \
+    if (theory::TheoryTraits<THEORY>::hasPresolve) { \
       reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \
       if(!d_theoryOut.d_conflictNode.get().isNull()) { \
         return true; \
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 8527924da..fc0f32927 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -15,7 +15,9 @@ libuf_la_SOURCES = \
 	theory_uf_type_rules.h \
 	theory_uf_rewriter.h \
 	equality_engine.h \
-	equality_engine_impl.h
+	equality_engine_impl.h \
+	symmetry_breaker.h \
+	symmetry_breaker.cpp
 
 libuf_la_LIBADD = \
 	@builddir@/tim/libuftim.la \
diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index e15467bff..01bab53ac 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -20,6 +20,7 @@
 #include "theory/valuation.h"
 #include "expr/kind.h"
 #include "util/congruence_closure.h"
+#include "theory/uf/symmetry_breaker.h"
 
 #include <map>
 
@@ -559,6 +560,15 @@ void TheoryUFMorgan::presolve() {
   TimerStat::CodeTimer codeTimer(d_presolveTimer);
 
   Debug("uf") << "uf: begin presolve()" << endl;
+  if(Options::current()->ufSymmetryBreaker) {
+    vector<Node> newClauses;
+    d_symb.apply(newClauses);
+    for(vector<Node>::const_iterator i = newClauses.begin();
+        i != newClauses.end();
+        ++i) {
+      d_out->lemma(*i);
+    }
+  }
   Debug("uf") << "uf: end presolve()" << endl;
 }
 
@@ -699,6 +709,10 @@ void TheoryUFMorgan::staticLearning(TNode n, NodeBuilder<>& learned) {
       }
     }
   }
+
+  if(Options::current()->ufSymmetryBreaker) {
+    d_symb.assertFormula(n);
+  }
 }
 
 /*
diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
index c2feef349..e801f383e 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.h
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -31,6 +31,7 @@
 #include "theory/theory.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/morgan/union_find.h"
+#include "theory/uf/symmetry_breaker.h"
 
 #include "context/context.h"
 #include "context/context_mm.h"
@@ -66,6 +67,8 @@ private:
    */
   context::CDList<Node> d_assertions;
 
+  SymmetryBreaker d_symb;
+
   /**
    * Our channel connected to the congruence closure module.
    */
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
new file mode 100644
index 000000000..1c2e8cd0d
--- /dev/null
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -0,0 +1,616 @@
+/*********************                                                        */
+/*! \file symmetry_breaker.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief Implementation of algorithm suggested by Deharbe, Fontaine,
+ ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011
+ **
+ ** Implementation of algorithm suggested by Deharbe, Fontaine, Merz,
+ ** and Paleo, "Exploiting symmetry in SMT problems," CADE 2011.
+ **
+ ** From the paper:
+ **
+ ** <pre>
+ **   P := guess_permutations(phi)
+ **   foreach {c_0, ..., c_n} \in P do
+ **     if invariant_by_permutations(phi, {c_0, ..., c_n}) then
+ **       T := select_terms(phi, {c_0, ..., c_n})
+ **       cts := \empty
+ **       while T != \empty && |cts| <= n do
+ **         t := select_most_promising_term(T, phi)
+ **         T := T \ {t}
+ **         cts := cts \cup used_in(t, {c_0, ..., c_n})
+ **         let c \in {c_0, ..., c_n} \ cts
+ **         cts := cts \cup {c}
+ **         if cts != {c_0, ..., c_n} then
+ **           phi := phi /\ ( \vee_{c_i \in cts} t = c_i )
+ **         end
+ **       end
+ **     end
+ **   end
+ **   return phi
+ ** </pre>
+ **/
+
+#include "theory/uf/symmetry_breaker.h"
+#include "theory/rewriter.h"
+#include "util/hash.h"
+
+#include <iterator>
+#include <queue>
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+SymmetryBreaker::Template::Template() :
+  d_template(),
+  d_sets(),
+  d_reps() {
+}
+
+TNode SymmetryBreaker::Template::find(TNode n) {
+  hash_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n);
+  if(i == d_reps.end()) {
+    return n;
+  } else {
+    return d_reps[n] = find((*i).second);
+  }
+}
+
+bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n) {
+  IndentedScope scope(Debug("ufsymm:match"));
+
+  Debug("ufsymm:match") << "UFSYMM matching " << t << endl
+                        << "UFSYMM       to " << n << endl;
+
+  if(t.getKind() != n.getKind() || t.getNumChildren() != n.getNumChildren()) {
+    Debug("ufsymm:match") << "UFSYMM BAD MATCH on kind, #children" << endl;
+    return false;
+  }
+
+  if(t.getNumChildren() == 0) {
+    if(t.getMetaKind() == kind::metakind::CONSTANT) {
+      Assert(n.getMetaKind() == kind::metakind::CONSTANT);
+      Debug("ufsymm:match") << "UFSYMM we have constants, failing match" << endl;
+      return false;
+    }
+    Assert(t.getMetaKind() == kind::metakind::VARIABLE &&
+           n.getMetaKind() == kind::metakind::VARIABLE);
+    t = find(t);
+    n = find(n);
+    Debug("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl;
+    Debug("ufsymm:match") << "UFSYMM sets: " << t << " =>";
+    if(d_sets.find(t) != d_sets.end()) {
+      for(set<TNode>::iterator i = d_sets[t].begin(); i != d_sets[t].end(); ++i) {
+        Debug("ufsymm:match") << " " << *i;
+      }
+    }
+    Debug("ufsymm:match") << endl;
+    if(t != n) {
+      Debug("ufsymm:match") << "UFSYMM sets: " << n << " =>";
+      if(d_sets.find(n) != d_sets.end()) {
+        for(set<TNode>::iterator i = d_sets[n].begin(); i != d_sets[n].end(); ++i) {
+          Debug("ufsymm:match") << " " << *i;
+        }
+      }
+      Debug("ufsymm:match") << endl;
+
+      if(d_sets.find(t) == d_sets.end()) {
+        Debug("ufsymm:match") << "UFSYMM inserting " << t << " in with " << n << endl;
+        d_reps[t] = n;
+        d_sets[n].insert(t);
+      } else {
+        if(d_sets.find(n) != d_sets.end()) {
+          Debug("ufsymm:match") << "UFSYMM merging " << n << " and " << t << " in with " << n << endl;
+          d_sets[n].insert(d_sets[t].begin(), d_sets[t].end());
+          d_sets[n].insert(t);
+          d_reps[t] = n;
+          d_sets.erase(t);
+        } else {
+          Debug("ufsymm:match") << "UFSYMM inserting " << n << " in with " << t << endl;
+          d_sets[t].insert(n);
+          d_reps[n] = t;
+        }
+      }
+    }
+    return true;
+  }
+
+  if(t.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    if(t.getOperator() != n.getOperator()) {
+      Debug("ufsymm:match") << "UFSYMM BAD MATCH on operators: " << t.getOperator() << " != " << n.getOperator() << endl;
+      return false;
+    }
+  }
+  TNode::iterator ti = t.begin();
+  TNode::iterator ni = n.begin();
+  while(ti != t.end()) {
+    if(*ti != *ni) { // nothing to do if equal
+      if(!matchRecursive(*ti, *ni)) {
+        Debug("ufsymm:match") << "UFSYMM BAD MATCH, withdrawing.." << endl;
+        return false;
+      }
+    }
+    ++ti;
+    ++ni;
+  }
+
+  return true;
+}
+
+bool SymmetryBreaker::Template::match(TNode n) {
+  // try to "match" n and d_template
+  if(d_template.isNull()) {
+    Debug("ufsymm") << "UFSYMM setting template " << n << endl;
+    d_template = n;
+    return true;
+  } else {
+    return matchRecursive(d_template, n);
+  }
+}
+
+void SymmetryBreaker::Template::reset() {
+  d_template = Node::null();
+  d_sets.clear();
+  d_reps.clear();
+}
+
+SymmetryBreaker::SymmetryBreaker() :
+  d_phi(),
+  d_phiSet(),
+  d_permutations(),
+  d_terms(),
+  d_template(),
+  d_normalizationCache(),
+  d_termEqs() {
+}
+
+Node SymmetryBreaker::norm(TNode phi) {
+  Node n = Rewriter::rewrite(phi);
+  return normInternal(n);
+}
+
+Node SymmetryBreaker::normInternal(TNode n) {
+  Node& result = d_normalizationCache[n];
+  if(!result.isNull()) {
+    return result;
+  }
+
+  switch(Kind k = n.getKind()) {
+
+  case kind::DISTINCT: {
+    // commutative N-ary operator handling
+    vector<TNode> kids(n.begin(), n.end());
+    sort(kids.begin(), kids.end());
+    return result = NodeManager::currentNM()->mkNode(k, kids);
+  }
+
+  case kind::AND:
+  case kind::OR: {
+    // commutative+associative N-ary operator handling
+    vector<Node> kids;
+    kids.reserve(n.getNumChildren());
+    queue<TNode> work;
+    work.push(n);
+    Debug("ufsymm:norm") << "UFSYMM processing " << n << endl;
+    do {
+      TNode m = work.front();
+      work.pop();
+      for(TNode::iterator i = m.begin(); i != m.end(); ++i) {
+        if((*i).getKind() == k) {
+          work.push(*i);
+        } else {
+          if( (*i).getKind() == kind::AND ||
+              (*i).getKind() == kind::OR ) {
+            kids.push_back(normInternal(*i));
+          } else if((*i).getKind() == kind::IFF ||
+                    (*i).getKind() == kind::EQUAL) {
+            kids.push_back(normInternal(*i));
+            if((*i)[0].getMetaKind() == kind::metakind::VARIABLE ||
+               (*i)[1].getMetaKind() == kind::metakind::VARIABLE) {
+              d_termEqs[(*i)[0]].insert((*i)[1]);
+              d_termEqs[(*i)[1]].insert((*i)[0]);
+              Debug("ufsymm:eq") << "UFSYMM " << (*i)[0] << " <==> " << (*i)[1] << endl;
+            }
+          } else {
+            kids.push_back(*i);
+          }
+        }
+      }
+    } while(!work.empty());
+    Debug("ufsymm:norm") << "UFSYMM got " << kids.size() << " kids for the " << k << "-kinded Node" << endl;
+    sort(kids.begin(), kids.end());
+    return result = NodeManager::currentNM()->mkNode(k, kids);
+  }
+
+  case kind::IFF:
+  case kind::EQUAL:
+    if(n[0].getMetaKind() == kind::metakind::VARIABLE ||
+       n[1].getMetaKind() == kind::metakind::VARIABLE) {
+      d_termEqs[n[0]].insert(n[1]);
+      d_termEqs[n[1]].insert(n[0]);
+      Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl;
+    }
+    /* intentional fall-through! */
+  case kind::XOR:
+    // commutative binary operator handling
+    return n[1] < n[0] ? NodeManager::currentNM()->mkNode(k, n[1], n[0]) : Node(n);
+
+  default:
+    // Normally T-rewriting is enough; only special cases (like
+    // Boolean-layer stuff) has to go above.
+    return n;
+  }
+}
+
+void SymmetryBreaker::assertFormula(TNode phi) {
+  // use d_phi, put into d_permutations
+  Debug("ufsymm") << "UFSYMM assertFormula(): phi is " << phi << endl;
+  d_phi.push_back(phi);
+  if(phi.getKind() == kind::OR) {
+    Template t;
+    Node::iterator i = phi.begin();
+    t.match(*i++);
+    while(i != phi.end()) {
+      if(!t.match(*i++)) {
+        break;
+      }
+    }
+    hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions();
+    for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
+        i != ps.end();
+        ++i) {
+      Debug("ufsymm") << "UFSYMM partition*: " << (*i).first;
+      set<TNode>& p = (*i).second;
+      for(set<TNode>::iterator j = p.begin();
+          j != p.end();
+          ++j) {
+        Debug("ufsymm") << " " << *j;
+      }
+      Debug("ufsymm") << endl;
+      p.insert((*i).first);
+      Permutations::iterator pi = d_permutations.find(p);
+      if(pi == d_permutations.end()) {
+        d_permutations.insert(p);
+      }
+    }
+  }
+  if(!d_template.match(phi)) {
+    // we hit a bad match, extract the partitions and reset the template
+    hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions();
+    Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl;
+    for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
+        i != ps.end();
+        ++i) {
+      Debug("ufsymm") << "UFSYMM partition: " << (*i).first;
+      set<TNode>& p = (*i).second;
+      if(Debug.isOn("ufsymm")) {
+        for(set<TNode>::iterator j = p.begin();
+            j != p.end();
+            ++j) {
+          Debug("ufsymm") << " " << *j;
+        }
+      }
+      Debug("ufsymm") << endl;
+      p.insert((*i).first);
+      d_permutations.insert(p);
+    }
+    d_template.reset();
+    bool good CVC4_UNUSED = d_template.match(phi);
+    Assert(good);
+  }
+}
+
+void SymmetryBreaker::clear() {
+  d_phi.clear();
+  d_phiSet.clear();
+  d_permutations.clear();
+  d_terms.clear();
+  d_template.reset();
+  d_normalizationCache.clear();
+  d_termEqs.clear();
+}
+
+void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
+  guessPermutations();
+  Debug("ufsymm") << "UFSYMM =====================================================" << endl
+                  << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl;
+  if(!d_permutations.empty()) {
+    { TimerStat::CodeTimer codeTimer(d_initNormalizationTimer);
+      // normalize d_phi
+
+      for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) {
+        Node n = *i;
+        *i = norm(n);
+        d_phiSet.insert(*i);
+        Debug("ufsymm:norm") << "UFSYMM init-norm-rewrite " << n << endl
+                             << "UFSYMM                to " << *i << endl;
+      }
+    }
+
+    for(Permutations::iterator i = d_permutations.begin();
+        i != d_permutations.end();
+        ++i) {
+      ++d_permutationSetsConsidered;
+      const Permutation& p = *i;
+      Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl;
+      size_t n = p.size() - 1;
+      if(invariantByPermutations(p)) {
+        ++d_permutationSetsInvariant;
+        selectTerms(p);
+        set<Node> cts;
+        while(!d_terms.empty() && cts.size() <= n) {
+          Debug("ufsymm") << "UFSYMM ==== top of loop, d_terms.size() == " << d_terms.size() << " , cts.size() == " << cts.size() << " , n == " << n << endl;
+          Terms::iterator ti = selectMostPromisingTerm(d_terms);
+          Node t = *ti;
+          Debug("ufsymm") << "UFSYMM promising term is " << t << endl;
+          d_terms.erase(ti);
+          insertUsedIn(t, p, cts);
+          if(Debug.isOn("ufsymm")) {
+            if(cts.empty()) {
+              Debug("ufsymm") << "UFSYMM cts is empty" << endl;
+            } else {
+              for(set<Node>::iterator ctsi = cts.begin(); ctsi != cts.end(); ++ctsi) {
+                Debug("ufsymm") << "UFSYMM cts: " << *ctsi << endl;
+              }
+            }
+          }
+          TNode c;
+          Debug("ufsymm") << "UFSYMM looking for c \\in " << p << " \\ cts" << endl;
+          set<TNode>::const_iterator i;
+          for(i = p.begin(); i != p.end(); ++i) {
+            if(cts.find(*i) == cts.end()) {
+              if(c.isNull()) {
+                c = *i;
+                Debug("ufsymm") << "UFSYMM found first: " << c << endl;
+              } else {
+                Debug("ufsymm") << "UFSYMM found second: " << *i << endl;
+                break;
+              }
+            }
+          }
+          if(c.isNull()) {
+            Debug("ufsymm") << "UFSYMM can't find a c, restart outer loop" << endl;
+            break;
+          }
+          Debug("ufsymm") << "UFSYMM inserting into cts: " << c << endl;
+          cts.insert(c);
+          // This tests cts != p: if "i == p.end()", we got all the way
+          // through p without seeing two elements not in cts (on the
+          // second one, we break from the above loop).  We know we
+          // found at least one (and subsequently added it to cts).  So
+          // now cts == p.
+          Debug("ufsymm") << "UFSYMM p == " << p << endl;
+          if(i != p.end() || p.size() != cts.size()) {
+            Debug("ufsymm") << "UFSYMM cts != p" << endl;
+            NodeBuilder<> disj(kind::OR);
+            for(set<Node>::const_iterator i = cts.begin();
+                i != cts.end();
+                ++i) {
+              if(t != *i) {
+                disj << NodeManager::currentNM()->mkNode(kind::EQUAL, t, *i);
+              }
+            }
+            Node d;
+            if(disj.getNumChildren() > 1) {
+              d = disj;
+              ++d_clauses;
+            } else {
+              d = disj[0];
+              disj.clear();
+              ++d_units;
+            }
+            if(Debug.isOn("ufsymm")) {
+              Debug("ufsymm") << "UFSYMM symmetry-breaking clause: " << d << endl;
+            } else {
+              Debug("ufsymm:clauses") << "UFSYMM symmetry-breaking clause: " << d << endl;
+            }
+            newClauses.push_back(d);
+          } else {
+            Debug("ufsymm") << "UFSYMM cts == p" << endl;
+          }
+          Debug("ufsymm") << "UFSYMM ==== end of loop, d_terms.size() == " << d_terms.size() << " , cts.size() == " << cts.size() << " , n == " << n << endl;
+        }
+      }
+    }
+  }
+
+  clear();
+}
+
+void SymmetryBreaker::guessPermutations() {
+  // use d_phi, put into d_permutations
+  Debug("ufsymm") << "UFSYMM guessPermutations()" << endl;
+}
+
+bool SymmetryBreaker::invariantByPermutations(const Permutation& p) {
+  TimerStat::CodeTimer codeTimer(d_invariantByPermutationsTimer);
+
+  // use d_phi
+  Debug("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl;
+
+  Assert(p.size() > 1);
+
+  // check P_swap
+  vector<Node> subs;
+  vector<Node> repls;
+  Permutation::iterator i = p.begin();
+  TNode p0 = *i++;
+  TNode p1 = *i;
+  subs.push_back(p0);
+  subs.push_back(p1);
+  repls.push_back(p1);
+  repls.push_back(p0);
+  for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) {
+    Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
+    Node n = norm(s);
+    if(*i != n && d_phiSet.find(n) == d_phiSet.end()) {
+      Debug("ufsymm") << "UFSYMM P_swap is NOT an inv perm op for " << p << endl
+                      << "UFSYMM because this node: " << *i << endl
+                      << "UFSYMM rewrite-norms to : " << n << endl
+                      << "UFSYMM which is not in our set of normalized assertions" << endl;
+      return false;
+    } else if(Debug.isOn("ufsymm:p")) {
+      if(*i == s) {
+        Debug("ufsymm:p") << "UFSYMM P_swap passes trivially: " << *i << endl;
+      } else {
+        Debug("ufsymm:p") << "UFSYMM P_swap passes: " << *i << endl
+                          << "UFSYMM      rewrites: " << s << endl
+                          << "UFSYMM         norms: " << n << endl;
+      }
+    }
+  }
+  Debug("ufsymm") << "UFSYMM P_swap is an inv perm op for " << p << endl;
+
+  // check P_circ, unless size == 2 in which case P_circ == P_swap
+  if(p.size() > 2) {
+    subs.clear();
+    repls.clear();
+    bool first = true;
+    for(Permutation::const_iterator i = p.begin(); i != p.end(); ++i) {
+      subs.push_back(*i);
+      if(!first) {
+        repls.push_back(*i);
+      } else {
+        first = false;
+      }
+    }
+    repls.push_back(*p.begin());
+    Assert(subs.size() == repls.size());
+    for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) {
+      Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
+      Node n = norm(s);
+      if(*i != n && d_phiSet.find(n) == d_phiSet.end()) {
+        Debug("ufsymm") << "UFSYMM P_circ is NOT an inv perm op for " << p << endl
+                        << "UFSYMM because this node: " << *i << endl
+                        << "UFSYMM rewrite-norms to : " << n << endl
+                        << "UFSYMM which is not in our set of normalized assertions" << endl;
+        return false;
+      } else if(Debug.isOn("ufsymm:p")) {
+        if(*i == s) {
+          Debug("ufsymm:p") << "UFSYMM P_circ passes trivially: " << *i << endl;
+        } else {
+          Debug("ufsymm:p") << "UFSYMM P_circ passes: " << *i << endl
+                            << "UFSYMM      rewrites: " << s << endl
+                            << "UFSYMM         norms: " << n << endl;
+        }
+      }
+    }
+    Debug("ufsymm") << "UFSYMM P_circ is an inv perm op for " << p << endl;
+  } else {
+    Debug("ufsymm") << "UFSYMM no need to check P_circ, since P_circ == P_swap for perm sets of size 2" << endl;
+  }
+
+  return true;
+}
+
+// debug-assertion-only function
+template <class T1, class T2>
+static bool isSubset(const T1& s, const T2& t) {
+  if(s.size() > t.size()) {
+    //Debug("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t "
+    //                << "because size(s) > size(t)" << endl;
+    return false;
+  }
+  for(typename T1::const_iterator si = s.begin(); si != s.end(); ++si) {
+    if(t.find(*si) == t.end()) {
+      //Debug("ufsymm") << "DEBUG ASSERTION FAIL: s not a subset of t "
+      //                << "because s element \"" << *si << "\" not in t" << endl;
+      return false;
+    }
+  }
+
+  // At this point, didn't find any elements from s not in t, so
+  // conclude that s \subseteq t
+  return true;
+}
+
+void SymmetryBreaker::selectTerms(const Permutation& p) {
+  TimerStat::CodeTimer codeTimer(d_selectTermsTimer);
+
+  // use d_phi, put into d_terms
+  Debug("ufsymm") << "UFSYMM selectTerms(): " << p << endl;
+  d_terms.clear();
+  set<Node> terms;
+  for(Permutation::iterator i = p.begin(); i != p.end(); ++i) {
+    const TermEq& teq = d_termEqs[*i];
+    terms.insert(teq.begin(), teq.end());
+  }
+  for(set<Node>::iterator i = terms.begin(); i != terms.end(); ++i) {
+    const TermEq& teq = d_termEqs[*i];
+    if(isSubset(teq, p)) {
+      d_terms.insert(d_terms.end(), *i);
+    } else {
+      if(Debug.isOn("ufsymm")) {
+        Debug("ufsymm") << "UFSYMM selectTerms() threw away candidate: " << *i << endl;
+        Debug("ufsymm:eq") << "UFSYMM selectTerms() #teq == " << teq.size() << " #p == " << p.size() << endl;
+        TermEq::iterator j;
+        for(j = teq.begin(); j != teq.end(); ++j) {
+          Debug("ufsymm:eq") << "UFSYMM              -- teq " << *j << " in " << p << " ?" << endl;
+          if(p.find(*j) == p.end()) {
+            Debug("ufsymm") << "UFSYMM              -- because its teq " << *j
+                            << " isn't in " << p << endl;
+            break;
+          } else {
+            Debug("ufsymm:eq") << "UFSYMM              -- yep" << endl;
+          }
+        }
+        Assert(j != teq.end(), "failed to find a difference between p and teq ?!");
+      }
+    }
+  }
+  if(Debug.isOn("ufsymm")) {
+    for(list<Term>::iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
+      Debug("ufsymm") << "UFSYMM selectTerms() returning: " << *i << endl;
+    }
+  }
+}
+
+SymmetryBreaker::Terms::iterator
+SymmetryBreaker::selectMostPromisingTerm(Terms& terms) {
+  // use d_phi
+  Debug("ufsymm") << "UFSYMM selectMostPromisingTerm()" << endl;
+  return terms.begin();
+}
+
+void SymmetryBreaker::insertUsedIn(Term term, const Permutation& p, set<Node>& cts) {
+  // insert terms from p used in term into cts
+  //Debug("ufsymm") << "UFSYMM usedIn(): " << term << " , " << p << endl;
+  if(find(p.begin(), p.end(), term) != p.end()) {
+    cts.insert(term);
+  } else {
+    for(TNode::iterator i = term.begin(); i != term.end(); ++i) {
+      insertUsedIn(*i, p, cts);
+    }
+  }
+}
+
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, const theory::uf::SymmetryBreaker::Permutation& p) {
+  out << "{";
+  set<TNode>::const_iterator i = p.begin();
+  while(i != p.end()) {
+    out << *i;
+    if(++i != p.end()) {
+      out << ",";
+    }
+  }
+  out << "}";
+  return out;
+}
+
+}/* CVC4 namespace */
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
new file mode 100644
index 000000000..1b2680cf3
--- /dev/null
+++ b/src/theory/uf/symmetry_breaker.h
@@ -0,0 +1,160 @@
+/*********************                                                        */
+/*! \file symmetry_breaker.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief Implementation of algorithm suggested by Deharbe, Fontaine,
+ ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011
+ **
+ ** Implementation of algorithm suggested by Deharbe, Fontaine,
+ ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011.
+ **
+ ** From the paper:
+ **
+ ** <pre>
+ **   P := guess_permutations(phi)
+ **   foreach {c_0, ..., c_n} \in P do
+ **     if invariant_by_permutations(phi, {c_0, ..., c_n}) then
+ **       T := select_terms(phi, {c_0, ..., c_n})
+ **       cts := \empty
+ **       while T != \empty && |cts| <= n do
+ **         t := select_most_promising_term(T, phi)
+ **         T := T \ {t}
+ **         cts := cts \cup used_in(t, {c_0, ..., c_n})
+ **         let c \in {c_0, ..., c_n} \ cts
+ **         cts := cts \cup {c}
+ **         if cts != {c_0, ..., c_n} then
+ **           phi := phi /\ ( \vee_{c_i \in cts} t = c_i )
+ **         end
+ **       end
+ **     end
+ **   end
+ **   return phi
+ ** </pre>
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__SYMMETRY_BREAKER_H
+#define __CVC4__THEORY__UF__SYMMETRY_BREAKER_H
+
+#include <iostream>
+#include <list>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "util/stats.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+class SymmetryBreaker {
+
+  class Template {
+    Node d_template;
+    NodeBuilder<> d_assertions;
+    std::hash_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets;
+    std::hash_map<TNode, TNode, TNodeHashFunction> d_reps;
+
+    TNode find(TNode n);
+    bool matchRecursive(TNode t, TNode n);
+
+  public:
+    Template();
+    bool match(TNode n);
+    std::hash_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; }
+    Node assertions() {
+      switch(d_assertions.getNumChildren()) {
+      case 0: return Node::null();
+      case 1: return d_assertions[0];
+      default: return Node(d_assertions);
+      }
+    }
+    void reset();
+  };/* class SymmetryBreaker::Template */
+
+public:
+
+  typedef std::set<TNode> Permutation;
+  typedef std::set<Permutation> Permutations;
+  typedef TNode Term;
+  typedef std::list<Term> Terms;
+  typedef std::set<Term> TermEq;
+  typedef std::hash_map<Term, TermEq, TNodeHashFunction> TermEqs;
+
+private:
+
+  std::vector<Node> d_phi;
+  std::set<TNode> d_phiSet;
+  Permutations d_permutations;
+  Terms d_terms;
+  Template d_template;
+  std::hash_map<Node, Node, NodeHashFunction> d_normalizationCache;
+  TermEqs d_termEqs;
+
+  void clear();
+
+  void guessPermutations();
+  bool invariantByPermutations(const Permutation& p);
+  void selectTerms(const Permutation& p);
+  Terms::iterator selectMostPromisingTerm(Terms& terms);
+  void insertUsedIn(Term term, const Permutation& p, std::set<Node>& cts);
+  Node normInternal(TNode phi);
+  Node norm(TNode n);
+
+  // === STATISTICS ===
+  /** number of new clauses that come from the SymmetryBreaker */
+  KEEP_STATISTIC(IntStat,
+                 d_clauses,
+                 "theory::uf::symmetry_breaker::clauses", 0);
+  /** number of new clauses that come from the SymmetryBreaker */
+  KEEP_STATISTIC(IntStat,
+                 d_units,
+                 "theory::uf::symmetry_breaker::units", 0);
+  /** number of potential permutation sets we found */
+  KEEP_STATISTIC(IntStat,
+                 d_permutationSetsConsidered,
+                 "theory::uf::symmetry_breaker::permutationSetsConsidered", 0);
+  /** number of invariant permutation sets we found */
+  KEEP_STATISTIC(IntStat,
+                 d_permutationSetsInvariant,
+                 "theory::uf::symmetry_breaker::permutationSetsInvariant", 0);
+  /** time spent in invariantByPermutations() */
+  KEEP_STATISTIC(TimerStat,
+                 d_invariantByPermutationsTimer,
+                 "theory::uf::symmetry_breaker::timers::invariantByPermutations");
+  /** time spent in selectTerms() */
+  KEEP_STATISTIC(TimerStat,
+                 d_selectTermsTimer,
+                 "theory::uf::symmetry_breaker::timers::selectTerms");
+  /** time spent in initial round of normalization */
+  KEEP_STATISTIC(TimerStat,
+                 d_initNormalizationTimer,
+                 "theory::uf::symmetry_breaker::timers::initNormalization");
+
+public:
+
+  SymmetryBreaker();
+  void assertFormula(TNode phi);
+  void apply(std::vector<Node>& newClauses);
+
+};/* class SymmetryBreaker */
+
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, const ::CVC4::theory::uf::SymmetryBreaker::Permutation& p);
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__UF__SYMMETRY_BREAKER_H */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9903acc57..0776ecf0d 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -227,6 +227,22 @@ void TheoryUF::explain(TNode literal) {
   d_out->explanation(mkAnd(assumptions));
 }
 
+void TheoryUF::presolve() {
+  // TimerStat::CodeTimer codeTimer(d_presolveTimer);
+
+  Debug("uf") << "uf: begin presolve()" << endl;
+  if(Options::current()->ufSymmetryBreaker) {
+    vector<Node> newClauses;
+    d_symb.apply(newClauses);
+    for(vector<Node>::const_iterator i = newClauses.begin();
+        i != newClauses.end();
+        ++i) {
+      d_out->lemma(*i);
+    }
+  }
+  Debug("uf") << "uf: end presolve()" << endl;
+}
+
 void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) {
   //TimerStat::CodeTimer codeTimer(d_staticLearningTimer);
 
@@ -334,4 +350,8 @@ void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) {
       }
     }
   }
+
+  if(Options::current()->ufSymmetryBreaker) {
+    d_symb.assertFormula(n);
+  }
 }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index eaab96f27..d78504dc8 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -27,6 +27,7 @@
 
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/uf/symmetry_breaker.h"
 
 #include "context/cdo.h"
 #include "context/cdset.h"
@@ -87,6 +88,9 @@ private:
   /** True node for predicates = false */
   Node d_false;
 
+  /** Symmetry analyzer */
+  SymmetryBreaker d_symb;
+
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
@@ -113,12 +117,13 @@ public:
   void preRegisterTerm(TNode term);
   void explain(TNode n);
 
+  void staticLearning(TNode in, NodeBuilder<>& learned);
+  void presolve();
+
   std::string identify() const {
     return "THEORY_UF";
   }
 
-  void staticLearning(TNode in, NodeBuilder<>& learned);
-
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */
diff --git a/src/util/options.cpp b/src/util/options.cpp
index ff028b6c6..9bceee931 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -88,7 +88,8 @@ Options::Options() :
   satRandomSeed(91648253),// Minisat's default value
   pivotRule(MINIMUM),
   arithPivotThreshold(16),
-  arithPropagateMaxLength(16)
+  arithPropagateMaxLength(16),
+  ufSymmetryBreaker(true)
 {
 }
 
@@ -97,6 +98,7 @@ static const string optionsDescription = "\
    --version | -V         identify this CVC4 binary\n\
    --help | -h            this command line reference\n\
    --parse-only           exit after parsing input\n\
+   --preprocess-only      exit after parsing preprocessing input (and dump preprocessed assertions, unless -q)\n\
    --mmap                 memory map file input\n\
    --show-config          show CVC4 static configuration\n\
    --segv-nospin          don't spin on segfault waiting for gdb\n\
@@ -129,6 +131,7 @@ static const string optionsDescription = "\
    --random-seed=S        sets the random seed for the sat solver\n\
    --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
    --disable-arithmetic-propagation turns on arithmetic propagation\n\
+   --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\
    --incremental          enable incremental solving\n";
 
 static const string languageDescription = "\
@@ -190,6 +193,7 @@ enum OptionValue {
   STATS,
   SEGV_NOSPIN,
   PARSE_ONLY,
+  PREPROCESS_ONLY,
   NO_CHECKING,
   NO_THEORY_REGISTRATION,
   USE_MMAP,
@@ -216,7 +220,8 @@ enum OptionValue {
   ARITHMETIC_VARIABLE_REMOVAL,
   ARITHMETIC_PROPAGATION,
   ARITHMETIC_PIVOT_THRESHOLD,
-  ARITHMETIC_PROP_MAX_LENGTH
+  ARITHMETIC_PROP_MAX_LENGTH,
+  DISABLE_SYMMETRY_BREAKER
 };/* enum OptionValue */
 
 /**
@@ -259,6 +264,7 @@ static struct option cmdlineOptions[] = {
   { "about"      , no_argument      , NULL, 'V'         },
   { "lang"       , required_argument, NULL, 'L'         },
   { "parse-only" , no_argument      , NULL, PARSE_ONLY  },
+  { "preprocess-only", no_argument  , NULL, PREPROCESS_ONLY  },
   { "mmap"       , no_argument      , NULL, USE_MMAP    },
   { "strict-parsing", no_argument   , NULL, STRICT_PARSING },
   { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
@@ -288,6 +294,7 @@ static struct option cmdlineOptions[] = {
   { "random-seed" , required_argument, NULL, RANDOM_SEED  },
   { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL },
   { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
+  { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -385,6 +392,10 @@ throw(OptionException) {
       parseOnly = true;
       break;
 
+    case PREPROCESS_ONLY:
+      preprocessOnly = true;
+      break;
+
     case NO_THEORY_REGISTRATION:
       theoryRegistration = false;
       break;
@@ -542,6 +553,10 @@ throw(OptionException) {
       arithPropagation = false;
       break;
 
+    case DISABLE_SYMMETRY_BREAKER:
+      ufSymmetryBreaker = false;
+      break;
+
     case RANDOM_SEED:
       satRandomSeed = atof(optarg);
       break;
diff --git a/src/util/options.h b/src/util/options.h
index 06ca20073..ce2bc71e7 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -89,6 +89,9 @@ struct CVC4_PUBLIC Options {
   /** Should we exit after parsing? */
   bool parseOnly;
 
+  /** Should we exit after preprocessing? */
+  bool preprocessOnly;
+
   /** Should the parser do semantic checks? */
   bool semanticChecks;
 
@@ -194,6 +197,12 @@ struct CVC4_PUBLIC Options {
    */
   uint16_t arithPropagateMaxLength;
 
+  /**
+   * Whether to do the symmetry-breaking preprocessing in UF as
+   * described by Deharbe et al. in CADE 2011 (on by default).
+   */
+  bool ufSymmetryBreaker;
+
   Options();
 
   /**
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 01eaee999..fd770e9f9 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -24,13 +24,15 @@ TESTS =	\
 	NEQ016_size5_reduced2b.smt \
 	dead_dnd002.smt \
 	iso_brn001.smt \
+	gensys_brn001.smt2 \
 	simple.01.cvc \
 	simple.02.cvc \
 	simple.03.cvc \
 	simple.04.cvc
 
 EXTRA_DIST = $(TESTS) \
-	euf_simp09.tim.smt
+	euf_simp09.tim.smt \
+	mkpidgeon
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
diff --git a/test/regress/regress0/uf/gensys_brn001.smt2 b/test/regress/regress0/uf/gensys_brn001.smt2
new file mode 100644
index 000000000..f3cc3c725
--- /dev/null
+++ b/test/regress/regress0/uf/gensys_brn001.smt2
@@ -0,0 +1,146 @@
+(set-logic QF_UF)
+(set-info :source |
+http://www.cs.bham.ac.uk/~vxs/quasigroups/benchmark/
+
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-sort U 0)
+(declare-sort I 0)
+(declare-fun unit () I)
+(declare-fun op (I I) I)
+(declare-fun e5 () I)
+(declare-fun e4 () I)
+(declare-fun e3 () I)
+(declare-fun e2 () I)
+(declare-fun e1 () I)
+(declare-fun e0 () I)
+(assert (let ((?v_0 (op e0 e0)) (?v_1 (op e0 e1)) (?v_2 (op e0 e2)) (?v_3 (op e0 e3)) (?v_4 (op e0 e4)) (?v_5 (op e0 e5)) (?v_6 (op e1 e0)) (?v_7 (op e1 e1)) (?v_8 (op e1 e2)) (?v_9 (op e1 e3)) (?v_10 (op e1 e4)) (?v_11 (op e1 e5)) (?v_12 (op e2 e0)) (?v_13 (op e2 e1)) (?v_14 (op e2 e2)) (?v_15 (op e2 e3)) (?v_16 (op e2 e4)) (?v_17 (op e2 e5)) (?v_18 (op e3 e0)) (?v_19 (op e3 e1)) (?v_20 (op e3 e2)) (?v_21 (op e3 e3)) (?v_22 (op e3 e4)) (?v_23 (op e3 e5)) (?v_24 (op e4 e0)) (?v_25 (op e4 e1)) (?v_26 (op e4 e2)) (?v_27 (op e4 e3)) (?v_28 (op e4 e4)) (?v_29 (op e4 e5)) (?v_30 (op e5 e0)) (?v_31 (op e5 e1)) (?v_32 (op e5 e2)) (?v_33 (op e5 e3)) (?v_34 (op e5 e4)) (?v_35 (op e5 e5))) (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (= ?v_0 e0) (= ?v_0 e1)) (= ?v_0 e2)) (= ?v_0 e3)) (= ?v_0 e4)) (= ?v_0 e5)) (or (or (or (or (or (= ?v_1 e0) (= ?v_1 e1)) (= ?v_1 e2)) (= ?v_1 e3)) (= ?v_1 e4)) (= ?v_1 e5))) (or (or (or (or (or (= ?v_2 e0) (= ?v_2 e1)) (= ?v_2 e2)) (= ?v_2 e3)) (= ?v_2 e4)) (= ?v_2 e5))) (or (or (or (or (or (= ?v_3 e0) (= ?v_3 e1)) (= ?v_3 e2)) (= ?v_3 e3)) (= ?v_3 e4)) (= ?v_3 e5))) (or (or (or (or (or (= ?v_4 e0) (= ?v_4 e1)) (= ?v_4 e2)) (= ?v_4 e3)) (= ?v_4 e4)) (= ?v_4 e5))) (or (or (or (or (or (= ?v_5 e0) (= ?v_5 e1)) (= ?v_5 e2)) (= ?v_5 e3)) (= ?v_5 e4)) (= ?v_5 e5))) (and (and (and (and (and (or (or (or (or (or (= ?v_6 e0) (= ?v_6 e1)) (= ?v_6 e2)) (= ?v_6 e3)) (= ?v_6 e4)) (= ?v_6 e5)) (or (or (or (or (or (= ?v_7 e0) (= ?v_7 e1)) (= ?v_7 e2)) (= ?v_7 e3)) (= ?v_7 e4)) (= ?v_7 e5))) (or (or (or (or (or (= ?v_8 e0) (= ?v_8 e1)) (= ?v_8 e2)) (= ?v_8 e3)) (= ?v_8 e4)) (= ?v_8 e5))) (or (or (or (or (or (= ?v_9 e0) (= ?v_9 e1)) (= ?v_9 e2)) (= ?v_9 e3)) (= ?v_9 e4)) (= ?v_9 e5))) (or (or (or (or (or (= ?v_10 e0) (= ?v_10 e1)) (= ?v_10 e2)) (= ?v_10 e3)) (= ?v_10 e4)) (= ?v_10 e5))) (or (or (or (or (or (= ?v_11 e0) (= ?v_11 e1)) (= ?v_11 e2)) (= ?v_11 e3)) (= ?v_11 e4)) (= ?v_11 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_12 e0) (= ?v_12 e1)) (= ?v_12 e2)) (= ?v_12 e3)) (= ?v_12 e4)) (= ?v_12 e5)) (or (or (or (or (or (= ?v_13 e0) (= ?v_13 e1)) (= ?v_13 e2)) (= ?v_13 e3)) (= ?v_13 e4)) (= ?v_13 e5))) (or (or (or (or (or (= ?v_14 e0) (= ?v_14 e1)) (= ?v_14 e2)) (= ?v_14 e3)) (= ?v_14 e4)) (= ?v_14 e5))) (or (or (or (or (or (= ?v_15 e0) (= ?v_15 e1)) (= ?v_15 e2)) (= ?v_15 e3)) (= ?v_15 e4)) (= ?v_15 e5))) (or (or (or (or (or (= ?v_16 e0) (= ?v_16 e1)) (= ?v_16 e2)) (= ?v_16 e3)) (= ?v_16 e4)) (= ?v_16 e5))) (or (or (or (or (or (= ?v_17 e0) (= ?v_17 e1)) (= ?v_17 e2)) (= ?v_17 e3)) (= ?v_17 e4)) (= ?v_17 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_18 e0) (= ?v_18 e1)) (= ?v_18 e2)) (= ?v_18 e3)) (= ?v_18 e4)) (= ?v_18 e5)) (or (or (or (or (or (= ?v_19 e0) (= ?v_19 e1)) (= ?v_19 e2)) (= ?v_19 e3)) (= ?v_19 e4)) (= ?v_19 e5))) (or (or (or (or (or (= ?v_20 e0) (= ?v_20 e1)) (= ?v_20 e2)) (= ?v_20 e3)) (= ?v_20 e4)) (= ?v_20 e5))) (or (or (or (or (or (= ?v_21 e0) (= ?v_21 e1)) (= ?v_21 e2)) (= ?v_21 e3)) (= ?v_21 e4)) (= ?v_21 e5))) (or (or (or (or (or (= ?v_22 e0) (= ?v_22 e1)) (= ?v_22 e2)) (= ?v_22 e3)) (= ?v_22 e4)) (= ?v_22 e5))) (or (or (or (or (or (= ?v_23 e0) (= ?v_23 e1)) (= ?v_23 e2)) (= ?v_23 e3)) (= ?v_23 e4)) (= ?v_23 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_24 e0) (= ?v_24 e1)) (= ?v_24 e2)) (= ?v_24 e3)) (= ?v_24 e4)) (= ?v_24 e5)) (or (or (or (or (or (= ?v_25 e0) (= ?v_25 e1)) (= ?v_25 e2)) (= ?v_25 e3)) (= ?v_25 e4)) (= ?v_25 e5))) (or (or (or (or (or (= ?v_26 e0) (= ?v_26 e1)) (= ?v_26 e2)) (= ?v_26 e3)) (= ?v_26 e4)) (= ?v_26 e5))) (or (or (or (or (or (= ?v_27 e0) (= ?v_27 e1)) (= ?v_27 e2)) (= ?v_27 e3)) (= ?v_27 e4)) (= ?v_27 e5))) (or (or (or (or (or (= ?v_28 e0) (= ?v_28 e1)) (= ?v_28 e2)) (= ?v_28 e3)) (= ?v_28 e4)) (= ?v_28 e5))) (or (or (or (or (or (= ?v_29 e0) (= ?v_29 e1)) (= ?v_29 e2)) (= ?v_29 e3)) (= ?v_29 e4)) (= ?v_29 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_30 e0) (= ?v_30 e1)) (= ?v_30 e2)) (= ?v_30 e3)) (= ?v_30 e4)) (= ?v_30 e5)) (or (or (or (or (or (= ?v_31 e0) (= ?v_31 e1)) (= ?v_31 e2)) (= ?v_31 e3)) (= ?v_31 e4)) (= ?v_31 e5))) (or (or (or (or (or (= ?v_32 e0) (= ?v_32 e1)) (= ?v_32 e2)) (= ?v_32 e3)) (= ?v_32 e4)) (= ?v_32 e5))) (or (or (or (or (or (= ?v_33 e0) (= ?v_33 e1)) (= ?v_33 e2)) (= ?v_33 e3)) (= ?v_33 e4)) (= ?v_33 e5))) (or (or (or (or (or (= ?v_34 e0) (= ?v_34 e1)) (= ?v_34 e2)) (= ?v_34 e3)) (= ?v_34 e4)) (= ?v_34 e5))) (or (or (or (or (or (= ?v_35 e0) (= ?v_35 e1)) (= ?v_35 e2)) (= ?v_35 e3)) (= ?v_35 e4)) (= ?v_35 e5))))))
+(assert (let ((?v_1 (op e0 e0)) (?v_2 (op e0 e1)) (?v_3 (op e0 e2)) (?v_4 (op e0 e3)) (?v_5 (op e0 e4)) (?v_6 (op e0 e5)) (?v_8 (op e1 e0)) (?v_21 (op e1 e1)) (?v_22 (op e1 e2)) (?v_23 (op e1 e3)) (?v_24 (op e1 e4)) (?v_25 (op e1 e5)) (?v_9 (op e2 e0)) (?v_28 (op e2 e1)) (?v_51 (op e2 e2)) (?v_52 (op e2 e3)) (?v_53 (op e2 e4)) (?v_54 (op e2 e5)) (?v_10 (op e3 e0)) (?v_29 (op e3 e1)) (?v_58 (op e3 e2)) (?v_91 (op e3 e3)) (?v_92 (op e3 e4)) (?v_93 (op e3 e5)) (?v_11 (op e4 e0)) (?v_30 (op e4 e1)) (?v_59 (op e4 e2)) (?v_98 (op e4 e3)) (?v_141 (op e4 e4)) (?v_142 (op e4 e5)) (?v_12 (op e5 e0)) (?v_31 (op e5 e1)) (?v_60 (op e5 e2)) (?v_99 (op e5 e3)) (?v_148 (op e5 e4)) (?v_201 (op e5 e5))) (let ((?v_0 (= ?v_1 e0)) (?v_7 (= ?v_1 e1)) (?v_13 (= ?v_1 e2)) (?v_14 (= ?v_1 e3)) (?v_15 (= ?v_1 e4)) (?v_16 (= ?v_1 e5)) (?v_18 (= ?v_2 e0)) (?v_26 (= ?v_2 e1)) (?v_33 (= ?v_2 e2)) (?v_36 (= ?v_2 e3)) (?v_39 (= ?v_2 e4)) (?v_42 (= ?v_2 e5)) (?v_46 (= ?v_3 e0)) (?v_55 (= ?v_3 e1)) (?v_63 (= ?v_3 e2)) (?v_68 (= ?v_3 e3)) (?v_73 (= ?v_3 e4)) (?v_78 (= ?v_3 e5)) (?v_84 (= ?v_4 e0)) (?v_94 (= ?v_4 e1)) (?v_103 (= ?v_4 e2)) (?v_110 (= ?v_4 e3)) (?v_117 (= ?v_4 e4)) (?v_124 (= ?v_4 e5)) (?v_132 (= ?v_5 e0)) (?v_143 (= ?v_5 e1)) (?v_153 (= ?v_5 e2)) (?v_162 (= ?v_5 e3)) (?v_171 (= ?v_5 e4)) (?v_180 (= ?v_5 e5)) (?v_190 (= ?v_6 e0)) (?v_202 (= ?v_6 e1)) (?v_213 (= ?v_6 e2)) (?v_224 (= ?v_6 e3)) (?v_235 (= ?v_6 e4)) (?v_246 (= ?v_6 e5)) (?v_17 (= ?v_8 e0)) (?v_20 (= ?v_8 e1)) (?v_32 (= ?v_8 e2)) (?v_35 (= ?v_8 e3)) (?v_38 (= ?v_8 e4)) (?v_41 (= ?v_8 e5)) (?v_19 (= ?v_21 e0)) (?v_27 (= ?v_21 e1)) (?v_34 (= ?v_21 e2)) (?v_37 (= ?v_21 e3)) (?v_40 (= ?v_21 e4)) (?v_43 (= ?v_21 e5)) (?v_47 (= ?v_22 e0)) (?v_56 (= ?v_22 e1)) (?v_64 (= ?v_22 e2)) (?v_69 (= ?v_22 e3)) (?v_74 (= ?v_22 e4)) (?v_79 (= ?v_22 e5)) (?v_85 (= ?v_23 e0)) (?v_95 (= ?v_23 e1)) (?v_104 (= ?v_23 e2)) (?v_111 (= ?v_23 e3)) (?v_118 (= ?v_23 e4)) (?v_125 (= ?v_23 e5)) (?v_133 (= ?v_24 e0)) (?v_144 (= ?v_24 e1)) (?v_154 (= ?v_24 e2)) (?v_163 (= ?v_24 e3)) (?v_172 (= ?v_24 e4)) (?v_181 (= ?v_24 e5)) (?v_191 (= ?v_25 e0)) (?v_203 (= ?v_25 e1)) (?v_214 (= ?v_25 e2)) (?v_225 (= ?v_25 e3)) (?v_236 (= ?v_25 e4)) (?v_247 (= ?v_25 e5)) (?v_44 (= ?v_9 e0)) (?v_49 (= ?v_9 e1)) (?v_61 (= ?v_9 e2)) (?v_66 (= ?v_9 e3)) (?v_71 (= ?v_9 e4)) (?v_76 (= ?v_9 e5)) (?v_45 (= ?v_28 e0)) (?v_50 (= ?v_28 e1)) (?v_62 (= ?v_28 e2)) (?v_67 (= ?v_28 e3)) (?v_72 (= ?v_28 e4)) (?v_77 (= ?v_28 e5)) (?v_48 (= ?v_51 e0)) (?v_57 (= ?v_51 e1)) (?v_65 (= ?v_51 e2)) (?v_70 (= ?v_51 e3)) (?v_75 (= ?v_51 e4)) (?v_80 (= ?v_51 e5)) (?v_86 (= ?v_52 e0)) (?v_96 (= ?v_52 e1)) (?v_105 (= ?v_52 e2)) (?v_112 (= ?v_52 e3)) (?v_119 (= ?v_52 e4)) (?v_126 (= ?v_52 e5)) (?v_134 (= ?v_53 e0)) (?v_145 (= ?v_53 e1)) (?v_155 (= ?v_53 e2)) (?v_164 (= ?v_53 e3)) (?v_173 (= ?v_53 e4)) (?v_182 (= ?v_53 e5)) (?v_192 (= ?v_54 e0)) (?v_204 (= ?v_54 e1)) (?v_215 (= ?v_54 e2)) (?v_226 (= ?v_54 e3)) (?v_237 (= ?v_54 e4)) (?v_248 (= ?v_54 e5)) (?v_81 (= ?v_10 e0)) (?v_88 (= ?v_10 e1)) (?v_100 (= ?v_10 e2)) (?v_107 (= ?v_10 e3)) (?v_114 (= ?v_10 e4)) (?v_121 (= ?v_10 e5)) (?v_82 (= ?v_29 e0)) (?v_89 (= ?v_29 e1)) (?v_101 (= ?v_29 e2)) (?v_108 (= ?v_29 e3)) (?v_115 (= ?v_29 e4)) (?v_122 (= ?v_29 e5)) (?v_83 (= ?v_58 e0)) (?v_90 (= ?v_58 e1)) (?v_102 (= ?v_58 e2)) (?v_109 (= ?v_58 e3)) (?v_116 (= ?v_58 e4)) (?v_123 (= ?v_58 e5)) (?v_87 (= ?v_91 e0)) (?v_97 (= ?v_91 e1)) (?v_106 (= ?v_91 e2)) (?v_113 (= ?v_91 e3)) (?v_120 (= ?v_91 e4)) (?v_127 (= ?v_91 e5)) (?v_135 (= ?v_92 e0)) (?v_146 (= ?v_92 e1)) (?v_156 (= ?v_92 e2)) (?v_165 (= ?v_92 e3)) (?v_174 (= ?v_92 e4)) (?v_183 (= ?v_92 e5)) (?v_193 (= ?v_93 e0)) (?v_205 (= ?v_93 e1)) (?v_216 (= ?v_93 e2)) (?v_227 (= ?v_93 e3)) (?v_238 (= ?v_93 e4)) (?v_249 (= ?v_93 e5)) (?v_128 (= ?v_11 e0)) (?v_137 (= ?v_11 e1)) (?v_149 (= ?v_11 e2)) (?v_158 (= ?v_11 e3)) (?v_167 (= ?v_11 e4)) (?v_176 (= ?v_11 e5)) (?v_129 (= ?v_30 e0)) (?v_138 (= ?v_30 e1)) (?v_150 (= ?v_30 e2)) (?v_159 (= ?v_30 e3)) (?v_168 (= ?v_30 e4)) (?v_177 (= ?v_30 e5)) (?v_130 (= ?v_59 e0)) (?v_139 (= ?v_59 e1)) (?v_151 (= ?v_59 e2)) (?v_160 (= ?v_59 e3)) (?v_169 (= ?v_59 e4)) (?v_178 (= ?v_59 e5)) (?v_131 (= ?v_98 e0)) (?v_140 (= ?v_98 e1)) (?v_152 (= ?v_98 e2)) (?v_161 (= ?v_98 e3)) (?v_170 (= ?v_98 e4)) (?v_179 (= ?v_98 e5)) (?v_136 (= ?v_141 e0)) (?v_147 (= ?v_141 e1)) (?v_157 (= ?v_141 e2)) (?v_166 (= ?v_141 e3)) (?v_175 (= ?v_141 e4)) (?v_184 (= ?v_141 e5)) (?v_194 (= ?v_142 e0)) (?v_206 (= ?v_142 e1)) (?v_217 (= ?v_142 e2)) (?v_228 (= ?v_142 e3)) (?v_239 (= ?v_142 e4)) (?v_250 (= ?v_142 e5)) (?v_185 (= ?v_12 e0)) (?v_196 (= ?v_12 e1)) (?v_208 (= ?v_12 e2)) (?v_219 (= ?v_12 e3)) (?v_230 (= ?v_12 e4)) (?v_241 (= ?v_12 e5)) (?v_186 (= ?v_31 e0)) (?v_197 (= ?v_31 e1)) (?v_209 (= ?v_31 e2)) (?v_220 (= ?v_31 e3)) (?v_231 (= ?v_31 e4)) (?v_242 (= ?v_31 e5)) (?v_187 (= ?v_60 e0)) (?v_198 (= ?v_60 e1)) (?v_210 (= ?v_60 e2)) (?v_221 (= ?v_60 e3)) (?v_232 (= ?v_60 e4)) (?v_243 (= ?v_60 e5)) (?v_188 (= ?v_99 e0)) (?v_199 (= ?v_99 e1)) (?v_211 (= ?v_99 e2)) (?v_222 (= ?v_99 e3)) (?v_233 (= ?v_99 e4)) (?v_244 (= ?v_99 e5)) (?v_189 (= ?v_148 e0)) (?v_200 (= ?v_148 e1)) (?v_212 (= ?v_148 e2)) (?v_223 (= ?v_148 e3)) (?v_234 (= ?v_148 e4)) (?v_245 (= ?v_148 e5)) (?v_195 (= ?v_201 e0)) (?v_207 (= ?v_201 e1)) (?v_218 (= ?v_201 e2)) (?v_229 (= ?v_201 e3)) (?v_240 (= ?v_201 e4)) (?v_251 (= ?v_201 e5))) (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or ?v_0 ?v_18) ?v_46) ?v_84) ?v_132) ?v_190) (or (or (or (or (or ?v_0 ?v_17) ?v_44) ?v_81) ?v_128) ?v_185)) (and (or (or (or (or (or ?v_7 ?v_26) ?v_55) ?v_94) ?v_143) ?v_202) (or (or (or (or (or ?v_7 ?v_20) ?v_49) ?v_88) ?v_137) ?v_196))) (and (or (or (or (or (or ?v_13 ?v_33) ?v_63) ?v_103) ?v_153) ?v_213) (or (or (or (or (or ?v_13 ?v_32) ?v_61) ?v_100) ?v_149) ?v_208))) (and (or (or (or (or (or ?v_14 ?v_36) ?v_68) ?v_110) ?v_162) ?v_224) (or (or (or (or (or ?v_14 ?v_35) ?v_66) ?v_107) ?v_158) ?v_219))) (and (or (or (or (or (or ?v_15 ?v_39) ?v_73) ?v_117) ?v_171) ?v_235) (or (or (or (or (or ?v_15 ?v_38) ?v_71) ?v_114) ?v_167) ?v_230))) (and (or (or (or (or (or ?v_16 ?v_42) ?v_78) ?v_124) ?v_180) ?v_246) (or (or (or (or (or ?v_16 ?v_41) ?v_76) ?v_121) ?v_176) ?v_241))) (and (and (and (and (and (and (or (or (or (or (or ?v_17 ?v_19) ?v_47) ?v_85) ?v_133) ?v_191) (or (or (or (or (or ?v_18 ?v_19) ?v_45) ?v_82) ?v_129) ?v_186)) (and (or (or (or (or (or ?v_20 ?v_27) ?v_56) ?v_95) ?v_144) ?v_203) (or (or (or (or (or ?v_26 ?v_27) ?v_50) ?v_89) ?v_138) ?v_197))) (and (or (or (or (or (or ?v_32 ?v_34) ?v_64) ?v_104) ?v_154) ?v_214) (or (or (or (or (or ?v_33 ?v_34) ?v_62) ?v_101) ?v_150) ?v_209))) (and (or (or (or (or (or ?v_35 ?v_37) ?v_69) ?v_111) ?v_163) ?v_225) (or (or (or (or (or ?v_36 ?v_37) ?v_67) ?v_108) ?v_159) ?v_220))) (and (or (or (or (or (or ?v_38 ?v_40) ?v_74) ?v_118) ?v_172) ?v_236) (or (or (or (or (or ?v_39 ?v_40) ?v_72) ?v_115) ?v_168) ?v_231))) (and (or (or (or (or (or ?v_41 ?v_43) ?v_79) ?v_125) ?v_181) ?v_247) (or (or (or (or (or ?v_42 ?v_43) ?v_77) ?v_122) ?v_177) ?v_242)))) (and (and (and (and (and (and (or (or (or (or (or ?v_44 ?v_45) ?v_48) ?v_86) ?v_134) ?v_192) (or (or (or (or (or ?v_46 ?v_47) ?v_48) ?v_83) ?v_130) ?v_187)) (and (or (or (or (or (or ?v_49 ?v_50) ?v_57) ?v_96) ?v_145) ?v_204) (or (or (or (or (or ?v_55 ?v_56) ?v_57) ?v_90) ?v_139) ?v_198))) (and (or (or (or (or (or ?v_61 ?v_62) ?v_65) ?v_105) ?v_155) ?v_215) (or (or (or (or (or ?v_63 ?v_64) ?v_65) ?v_102) ?v_151) ?v_210))) (and (or (or (or (or (or ?v_66 ?v_67) ?v_70) ?v_112) ?v_164) ?v_226) (or (or (or (or (or ?v_68 ?v_69) ?v_70) ?v_109) ?v_160) ?v_221))) (and (or (or (or (or (or ?v_71 ?v_72) ?v_75) ?v_119) ?v_173) ?v_237) (or (or (or (or (or ?v_73 ?v_74) ?v_75) ?v_116) ?v_169) ?v_232))) (and (or (or (or (or (or ?v_76 ?v_77) ?v_80) ?v_126) ?v_182) ?v_248) (or (or (or (or (or ?v_78 ?v_79) ?v_80) ?v_123) ?v_178) ?v_243)))) (and (and (and (and (and (and (or (or (or (or (or ?v_81 ?v_82) ?v_83) ?v_87) ?v_135) ?v_193) (or (or (or (or (or ?v_84 ?v_85) ?v_86) ?v_87) ?v_131) ?v_188)) (and (or (or (or (or (or ?v_88 ?v_89) ?v_90) ?v_97) ?v_146) ?v_205) (or (or (or (or (or ?v_94 ?v_95) ?v_96) ?v_97) ?v_140) ?v_199))) (and (or (or (or (or (or ?v_100 ?v_101) ?v_102) ?v_106) ?v_156) ?v_216) (or (or (or (or (or ?v_103 ?v_104) ?v_105) ?v_106) ?v_152) ?v_211))) (and (or (or (or (or (or ?v_107 ?v_108) ?v_109) ?v_113) ?v_165) ?v_227) (or (or (or (or (or ?v_110 ?v_111) ?v_112) ?v_113) ?v_161) ?v_222))) (and (or (or (or (or (or ?v_114 ?v_115) ?v_116) ?v_120) ?v_174) ?v_238) (or (or (or (or (or ?v_117 ?v_118) ?v_119) ?v_120) ?v_170) ?v_233))) (and (or (or (or (or (or ?v_121 ?v_122) ?v_123) ?v_127) ?v_183) ?v_249) (or (or (or (or (or ?v_124 ?v_125) ?v_126) ?v_127) ?v_179) ?v_244)))) (and (and (and (and (and (and (or (or (or (or (or ?v_128 ?v_129) ?v_130) ?v_131) ?v_136) ?v_194) (or (or (or (or (or ?v_132 ?v_133) ?v_134) ?v_135) ?v_136) ?v_189)) (and (or (or (or (or (or ?v_137 ?v_138) ?v_139) ?v_140) ?v_147) ?v_206) (or (or (or (or (or ?v_143 ?v_144) ?v_145) ?v_146) ?v_147) ?v_200))) (and (or (or (or (or (or ?v_149 ?v_150) ?v_151) ?v_152) ?v_157) ?v_217) (or (or (or (or (or ?v_153 ?v_154) ?v_155) ?v_156) ?v_157) ?v_212))) (and (or (or (or (or (or ?v_158 ?v_159) ?v_160) ?v_161) ?v_166) ?v_228) (or (or (or (or (or ?v_162 ?v_163) ?v_164) ?v_165) ?v_166) ?v_223))) (and (or (or (or (or (or ?v_167 ?v_168) ?v_169) ?v_170) ?v_175) ?v_239) (or (or (or (or (or ?v_171 ?v_172) ?v_173) ?v_174) ?v_175) ?v_234))) (and (or (or (or (or (or ?v_176 ?v_177) ?v_178) ?v_179) ?v_184) ?v_250) (or (or (or (or (or ?v_180 ?v_181) ?v_182) ?v_183) ?v_184) ?v_245)))) (and (and (and (and (and (and (or (or (or (or (or ?v_185 ?v_186) ?v_187) ?v_188) ?v_189) ?v_195) (or (or (or (or (or ?v_190 ?v_191) ?v_192) ?v_193) ?v_194) ?v_195)) (and (or (or (or (or (or ?v_196 ?v_197) ?v_198) ?v_199) ?v_200) ?v_207) (or (or (or (or (or ?v_202 ?v_203) ?v_204) ?v_205) ?v_206) ?v_207))) (and (or (or (or (or (or ?v_208 ?v_209) ?v_210) ?v_211) ?v_212) ?v_218) (or (or (or (or (or ?v_213 ?v_214) ?v_215) ?v_216) ?v_217) ?v_218))) (and (or (or (or (or (or ?v_219 ?v_220) ?v_221) ?v_222) ?v_223) ?v_229) (or (or (or (or (or ?v_224 ?v_225) ?v_226) ?v_227) ?v_228) ?v_229))) (and (or (or (or (or (or ?v_230 ?v_231) ?v_232) ?v_233) ?v_234) ?v_240) (or (or (or (or (or ?v_235 ?v_236) ?v_237) ?v_238) ?v_239) ?v_240))) (and (or (or (or (or (or ?v_241 ?v_242) ?v_243) ?v_244) ?v_245) ?v_251) (or (or (or (or (or ?v_246 ?v_247) ?v_248) ?v_249) ?v_250) ?v_251)))))))
+(assert (and (and (and (and (and (and (and (= (op unit e0) e0) (= (op e0 unit) e0)) (and (= (op unit e1) e1) (= (op e1 unit) e1))) (and (= (op unit e2) e2) (= (op e2 unit) e2))) (and (= (op unit e3) e3) (= (op e3 unit) e3))) (and (= (op unit e4) e4) (= (op e4 unit) e4))) (and (= (op unit e5) e5) (= (op e5 unit) e5))) (or (or (or (or (or (= unit e0) (= unit e1)) (= unit e2)) (= unit e3)) (= unit e4)) (= unit e5))))
+(assert (= unit e0))
+(assert (let ((?v_0 (op e0 e0)) (?v_6 (op e0 e1)) (?v_12 (op e0 e2)) (?v_18 (op e0 e3)) (?v_24 (op e0 e4)) (?v_30 (op e0 e5)) (?v_1 (op e1 e0)) (?v_7 (op e1 e1)) (?v_13 (op e1 e2)) (?v_19 (op e1 e3)) (?v_25 (op e1 e4)) (?v_31 (op e1 e5)) (?v_2 (op e2 e0)) (?v_8 (op e2 e1)) (?v_14 (op e2 e2)) (?v_20 (op e2 e3)) (?v_26 (op e2 e4)) (?v_32 (op e2 e5)) (?v_3 (op e3 e0)) (?v_9 (op e3 e1)) (?v_15 (op e3 e2)) (?v_21 (op e3 e3)) (?v_27 (op e3 e4)) (?v_33 (op e3 e5)) (?v_4 (op e4 e0)) (?v_10 (op e4 e1)) (?v_16 (op e4 e2)) (?v_22 (op e4 e3)) (?v_28 (op e4 e4)) (?v_34 (op e4 e5)) (?v_5 (op e5 e0)) (?v_11 (op e5 e1)) (?v_17 (op e5 e2)) (?v_23 (op e5 e3)) (?v_29 (op e5 e4)) (?v_35 (op e5 e5))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_0 ?v_1)) (not (= ?v_0 ?v_2))) (not (= ?v_0 ?v_3))) (not (= ?v_0 ?v_4))) (not (= ?v_0 ?v_5))) (not (= ?v_1 ?v_2))) (not (= ?v_1 ?v_3))) (not (= ?v_1 ?v_4))) (not (= ?v_1 ?v_5))) (not (= ?v_2 ?v_3))) (not (= ?v_2 ?v_4))) (not (= ?v_2 ?v_5))) (not (= ?v_3 ?v_4))) (not (= ?v_3 ?v_5))) (not (= ?v_4 ?v_5))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_6 ?v_7)) (not (= ?v_6 ?v_8))) (not (= ?v_6 ?v_9))) (not (= ?v_6 ?v_10))) (not (= ?v_6 ?v_11))) (not (= ?v_7 ?v_8))) (not (= ?v_7 ?v_9))) (not (= ?v_7 ?v_10))) (not (= ?v_7 ?v_11))) (not (= ?v_8 ?v_9))) (not (= ?v_8 ?v_10))) (not (= ?v_8 ?v_11))) (not (= ?v_9 ?v_10))) (not (= ?v_9 ?v_11))) (not (= ?v_10 ?v_11)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_12 ?v_13)) (not (= ?v_12 ?v_14))) (not (= ?v_12 ?v_15))) (not (= ?v_12 ?v_16))) (not (= ?v_12 ?v_17))) (not (= ?v_13 ?v_14))) (not (= ?v_13 ?v_15))) (not (= ?v_13 ?v_16))) (not (= ?v_13 ?v_17))) (not (= ?v_14 ?v_15))) (not (= ?v_14 ?v_16))) (not (= ?v_14 ?v_17))) (not (= ?v_15 ?v_16))) (not (= ?v_15 ?v_17))) (not (= ?v_16 ?v_17)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_18 ?v_19)) (not (= ?v_18 ?v_20))) (not (= ?v_18 ?v_21))) (not (= ?v_18 ?v_22))) (not (= ?v_18 ?v_23))) (not (= ?v_19 ?v_20))) (not (= ?v_19 ?v_21))) (not (= ?v_19 ?v_22))) (not (= ?v_19 ?v_23))) (not (= ?v_20 ?v_21))) (not (= ?v_20 ?v_22))) (not (= ?v_20 ?v_23))) (not (= ?v_21 ?v_22))) (not (= ?v_21 ?v_23))) (not (= ?v_22 ?v_23)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_24 ?v_25)) (not (= ?v_24 ?v_26))) (not (= ?v_24 ?v_27))) (not (= ?v_24 ?v_28))) (not (= ?v_24 ?v_29))) (not (= ?v_25 ?v_26))) (not (= ?v_25 ?v_27))) (not (= ?v_25 ?v_28))) (not (= ?v_25 ?v_29))) (not (= ?v_26 ?v_27))) (not (= ?v_26 ?v_28))) (not (= ?v_26 ?v_29))) (not (= ?v_27 ?v_28))) (not (= ?v_27 ?v_29))) (not (= ?v_28 ?v_29)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_30 ?v_31)) (not (= ?v_30 ?v_32))) (not (= ?v_30 ?v_33))) (not (= ?v_30 ?v_34))) (not (= ?v_30 ?v_35))) (not (= ?v_31 ?v_32))) (not (= ?v_31 ?v_33))) (not (= ?v_31 ?v_34))) (not (= ?v_31 ?v_35))) (not (= ?v_32 ?v_33))) (not (= ?v_32 ?v_34))) (not (= ?v_32 ?v_35))) (not (= ?v_33 ?v_34))) (not (= ?v_33 ?v_35))) (not (= ?v_34 ?v_35)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_0 ?v_6)) (not (= ?v_0 ?v_12))) (not (= ?v_0 ?v_18))) (not (= ?v_0 ?v_24))) (not (= ?v_0 ?v_30))) (not (= ?v_6 ?v_12))) (not (= ?v_6 ?v_18))) (not (= ?v_6 ?v_24))) (not (= ?v_6 ?v_30))) (not (= ?v_12 ?v_18))) (not (= ?v_12 ?v_24))) (not (= ?v_12 ?v_30))) (not (= ?v_18 ?v_24))) (not (= ?v_18 ?v_30))) (not (= ?v_24 ?v_30))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_1 ?v_7)) (not (= ?v_1 ?v_13))) (not (= ?v_1 ?v_19))) (not (= ?v_1 ?v_25))) (not (= ?v_1 ?v_31))) (not (= ?v_7 ?v_13))) (not (= ?v_7 ?v_19))) (not (= ?v_7 ?v_25))) (not (= ?v_7 ?v_31))) (not (= ?v_13 ?v_19))) (not (= ?v_13 ?v_25))) (not (= ?v_13 ?v_31))) (not (= ?v_19 ?v_25))) (not (= ?v_19 ?v_31))) (not (= ?v_25 ?v_31)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_2 ?v_8)) (not (= ?v_2 ?v_14))) (not (= ?v_2 ?v_20))) (not (= ?v_2 ?v_26))) (not (= ?v_2 ?v_32))) (not (= ?v_8 ?v_14))) (not (= ?v_8 ?v_20))) (not (= ?v_8 ?v_26))) (not (= ?v_8 ?v_32))) (not (= ?v_14 ?v_20))) (not (= ?v_14 ?v_26))) (not (= ?v_14 ?v_32))) (not (= ?v_20 ?v_26))) (not (= ?v_20 ?v_32))) (not (= ?v_26 ?v_32)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_3 ?v_9)) (not (= ?v_3 ?v_15))) (not (= ?v_3 ?v_21))) (not (= ?v_3 ?v_27))) (not (= ?v_3 ?v_33))) (not (= ?v_9 ?v_15))) (not (= ?v_9 ?v_21))) (not (= ?v_9 ?v_27))) (not (= ?v_9 ?v_33))) (not (= ?v_15 ?v_21))) (not (= ?v_15 ?v_27))) (not (= ?v_15 ?v_33))) (not (= ?v_21 ?v_27))) (not (= ?v_21 ?v_33))) (not (= ?v_27 ?v_33)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_4 ?v_10)) (not (= ?v_4 ?v_16))) (not (= ?v_4 ?v_22))) (not (= ?v_4 ?v_28))) (not (= ?v_4 ?v_34))) (not (= ?v_10 ?v_16))) (not (= ?v_10 ?v_22))) (not (= ?v_10 ?v_28))) (not (= ?v_10 ?v_34))) (not (= ?v_16 ?v_22))) (not (= ?v_16 ?v_28))) (not (= ?v_16 ?v_34))) (not (= ?v_22 ?v_28))) (not (= ?v_22 ?v_34))) (not (= ?v_28 ?v_34)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_5 ?v_11)) (not (= ?v_5 ?v_17))) (not (= ?v_5 ?v_23))) (not (= ?v_5 ?v_29))) (not (= ?v_5 ?v_35))) (not (= ?v_11 ?v_17))) (not (= ?v_11 ?v_23))) (not (= ?v_11 ?v_29))) (not (= ?v_11 ?v_35))) (not (= ?v_17 ?v_23))) (not (= ?v_17 ?v_29))) (not (= ?v_17 ?v_35))) (not (= ?v_23 ?v_29))) (not (= ?v_23 ?v_35))) (not (= ?v_29 ?v_35)))))))
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= e0 e1)) (not (= e0 e2))) (not (= e0 e3))) (not (= e0 e4))) (not (= e0 e5))) (not (= e1 e2))) (not (= e1 e3))) (not (= e1 e4))) (not (= e1 e5))) (not (= e2 e3))) (not (= e2 e4))) (not (= e2 e5))) (not (= e3 e4))) (not (= e3 e5))) (not (= e4 e5))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e1 e1))) (= e3 (op e4 e4))) (= e4 (op e5 e2))) (= e5 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e1 e1))) (= e3 (op e5 e5))) (= e5 (op e4 e2))) (= e4 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e1 e1))) (= e4 (op e3 e3))) (= e3 (op e5 e2))) (= e5 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e1 e1))) (= e4 (op e5 e5))) (= e5 (op e3 e2))) (= e3 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e1 e1))) (= e5 (op e3 e3))) (= e3 (op e4 e2))) (= e4 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e1 e1))) (= e5 (op e4 e4))) (= e4 (op e3 e2))) (= e3 (op e2 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e1 e1))) (= e2 (op e4 e4))) (= e4 (op e5 e3))) (= e5 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e1 e1))) (= e2 (op e5 e5))) (= e5 (op e4 e3))) (= e4 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e1 e1))) (= e4 (op e2 e2))) (= e2 (op e5 e3))) (= e5 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e1 e1))) (= e4 (op e5 e5))) (= e5 (op e2 e3))) (= e2 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e1 e1))) (= e5 (op e2 e2))) (= e2 (op e4 e3))) (= e4 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e1 e1))) (= e5 (op e4 e4))) (= e4 (op e2 e3))) (= e2 (op e3 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e1 e1))) (= e2 (op e3 e3))) (= e3 (op e5 e4))) (= e5 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e1 e1))) (= e2 (op e5 e5))) (= e5 (op e3 e4))) (= e3 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e1 e1))) (= e3 (op e2 e2))) (= e2 (op e5 e4))) (= e5 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e1 e1))) (= e3 (op e5 e5))) (= e5 (op e2 e4))) (= e2 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e1 e1))) (= e5 (op e2 e2))) (= e2 (op e3 e4))) (= e3 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e1 e1))) (= e5 (op e3 e3))) (= e3 (op e2 e4))) (= e2 (op e4 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e1 e1))) (= e2 (op e3 e3))) (= e3 (op e4 e5))) (= e4 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e1 e1))) (= e2 (op e4 e4))) (= e4 (op e3 e5))) (= e3 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e1 e1))) (= e3 (op e2 e2))) (= e2 (op e4 e5))) (= e4 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e1 e1))) (= e3 (op e4 e4))) (= e4 (op e2 e5))) (= e2 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e1 e1))) (= e4 (op e2 e2))) (= e2 (op e3 e5))) (= e3 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e1 e1))) (= e4 (op e3 e3))) (= e3 (op e2 e5))) (= e2 (op e5 e1)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e2 e2))) (= e3 (op e4 e4))) (= e4 (op e5 e1))) (= e5 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e2 e2))) (= e3 (op e5 e5))) (= e5 (op e4 e1))) (= e4 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e2 e2))) (= e4 (op e3 e3))) (= e3 (op e5 e1))) (= e5 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e2 e2))) (= e4 (op e5 e5))) (= e5 (op e3 e1))) (= e3 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e2 e2))) (= e5 (op e3 e3))) (= e3 (op e4 e1))) (= e4 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e2 e2))) (= e5 (op e4 e4))) (= e4 (op e3 e1))) (= e3 (op e1 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e2 e2))) (= e1 (op e4 e4))) (= e4 (op e5 e3))) (= e5 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e2 e2))) (= e1 (op e5 e5))) (= e5 (op e4 e3))) (= e4 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e2 e2))) (= e4 (op e1 e1))) (= e1 (op e5 e3))) (= e5 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e2 e2))) (= e4 (op e5 e5))) (= e5 (op e1 e3))) (= e1 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e2 e2))) (= e5 (op e1 e1))) (= e1 (op e4 e3))) (= e4 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e2 e2))) (= e5 (op e4 e4))) (= e4 (op e1 e3))) (= e1 (op e3 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e2 e2))) (= e1 (op e3 e3))) (= e3 (op e5 e4))) (= e5 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e2 e2))) (= e1 (op e5 e5))) (= e5 (op e3 e4))) (= e3 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e2 e2))) (= e3 (op e1 e1))) (= e1 (op e5 e4))) (= e5 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e2 e2))) (= e3 (op e5 e5))) (= e5 (op e1 e4))) (= e1 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e2 e2))) (= e5 (op e1 e1))) (= e1 (op e3 e4))) (= e3 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e2 e2))) (= e5 (op e3 e3))) (= e3 (op e1 e4))) (= e1 (op e4 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e2 e2))) (= e1 (op e3 e3))) (= e3 (op e4 e5))) (= e4 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e2 e2))) (= e1 (op e4 e4))) (= e4 (op e3 e5))) (= e3 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e2 e2))) (= e3 (op e1 e1))) (= e1 (op e4 e5))) (= e4 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e2 e2))) (= e3 (op e4 e4))) (= e4 (op e1 e5))) (= e1 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e2 e2))) (= e4 (op e1 e1))) (= e1 (op e3 e5))) (= e3 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e2 e2))) (= e4 (op e3 e3))) (= e3 (op e1 e5))) (= e1 (op e5 e2)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e3 e3))) (= e2 (op e4 e4))) (= e4 (op e5 e1))) (= e5 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e3 e3))) (= e2 (op e5 e5))) (= e5 (op e4 e1))) (= e4 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e3 e3))) (= e4 (op e2 e2))) (= e2 (op e5 e1))) (= e5 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e3 e3))) (= e4 (op e5 e5))) (= e5 (op e2 e1))) (= e2 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e3 e3))) (= e5 (op e2 e2))) (= e2 (op e4 e1))) (= e4 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e3 e3))) (= e5 (op e4 e4))) (= e4 (op e2 e1))) (= e2 (op e1 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e3 e3))) (= e1 (op e4 e4))) (= e4 (op e5 e2))) (= e5 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e3 e3))) (= e1 (op e5 e5))) (= e5 (op e4 e2))) (= e4 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e3 e3))) (= e4 (op e1 e1))) (= e1 (op e5 e2))) (= e5 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e3 e3))) (= e4 (op e5 e5))) (= e5 (op e1 e2))) (= e1 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e3 e3))) (= e5 (op e1 e1))) (= e1 (op e4 e2))) (= e4 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e3 e3))) (= e5 (op e4 e4))) (= e4 (op e1 e2))) (= e1 (op e2 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e3 e3))) (= e1 (op e2 e2))) (= e2 (op e5 e4))) (= e5 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e3 e3))) (= e1 (op e5 e5))) (= e5 (op e2 e4))) (= e2 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e3 e3))) (= e2 (op e1 e1))) (= e1 (op e5 e4))) (= e5 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e3 e3))) (= e2 (op e5 e5))) (= e5 (op e1 e4))) (= e1 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e3 e3))) (= e5 (op e1 e1))) (= e1 (op e2 e4))) (= e2 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e4 (op e3 e3))) (= e5 (op e2 e2))) (= e2 (op e1 e4))) (= e1 (op e4 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e3 e3))) (= e1 (op e2 e2))) (= e2 (op e4 e5))) (= e4 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e3 e3))) (= e1 (op e4 e4))) (= e4 (op e2 e5))) (= e2 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e3 e3))) (= e2 (op e1 e1))) (= e1 (op e4 e5))) (= e4 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e3 e3))) (= e2 (op e4 e4))) (= e4 (op e1 e5))) (= e1 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e3 e3))) (= e4 (op e1 e1))) (= e1 (op e2 e5))) (= e2 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e5 (op e3 e3))) (= e4 (op e2 e2))) (= e2 (op e1 e5))) (= e1 (op e5 e3)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e4 e4))) (= e2 (op e3 e3))) (= e3 (op e5 e1))) (= e5 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e4 e4))) (= e2 (op e5 e5))) (= e5 (op e3 e1))) (= e3 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e4 e4))) (= e3 (op e2 e2))) (= e2 (op e5 e1))) (= e5 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e4 e4))) (= e3 (op e5 e5))) (= e5 (op e2 e1))) (= e2 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e4 e4))) (= e5 (op e2 e2))) (= e2 (op e3 e1))) (= e3 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e1 (op e4 e4))) (= e5 (op e3 e3))) (= e3 (op e2 e1))) (= e2 (op e1 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e4 e4))) (= e1 (op e3 e3))) (= e3 (op e5 e2))) (= e5 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e4 e4))) (= e1 (op e5 e5))) (= e5 (op e3 e2))) (= e3 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e4 e4))) (= e3 (op e1 e1))) (= e1 (op e5 e2))) (= e5 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e4 e4))) (= e3 (op e5 e5))) (= e5 (op e1 e2))) (= e1 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e4 e4))) (= e5 (op e1 e1))) (= e1 (op e3 e2))) (= e3 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e2 (op e4 e4))) (= e5 (op e3 e3))) (= e3 (op e1 e2))) (= e1 (op e2 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e4 e4))) (= e1 (op e2 e2))) (= e2 (op e5 e3))) (= e5 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e4 e4))) (= e1 (op e5 e5))) (= e5 (op e2 e3))) (= e2 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e4 e4))) (= e2 (op e1 e1))) (= e1 (op e5 e3))) (= e5 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e4 e4))) (= e2 (op e5 e5))) (= e5 (op e1 e3))) (= e1 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e4 e4))) (= e5 (op e1 e1))) (= e1 (op e2 e3))) (= e2 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e3 (op e4 e4))) (= e5 (op e2 e2))) (= e2 (op e1 e3))) (= e1 (op e3 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e4 e4))) (= e1 (op e2 e2))) (= e2 (op e3 e5))) (= e3 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e5 (op e4 e4))) (= e1 (op e3 e3))) (= e3 (op e2 e5))) (= e2 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e4 e4))) (= e2 (op e1 e1))) (= e1 (op e3 e5))) (= e3 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e5 (op e4 e4))) (= e2 (op e3 e3))) (= e3 (op e1 e5))) (= e1 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e4 e4))) (= e3 (op e1 e1))) (= e1 (op e2 e5))) (= e2 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e5 (op e4 e4))) (= e3 (op e2 e2))) (= e2 (op e1 e5))) (= e1 (op e5 e4)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e5 e5))) (= e2 (op e3 e3))) (= e3 (op e4 e1))) (= e4 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e1 (op e5 e5))) (= e2 (op e4 e4))) (= e4 (op e3 e1))) (= e3 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e5 e5))) (= e3 (op e2 e2))) (= e2 (op e4 e1))) (= e4 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e1 (op e5 e5))) (= e3 (op e4 e4))) (= e4 (op e2 e1))) (= e2 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e5 e5))) (= e4 (op e2 e2))) (= e2 (op e3 e1))) (= e3 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e1 (op e5 e5))) (= e4 (op e3 e3))) (= e3 (op e2 e1))) (= e2 (op e1 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e5 e5))) (= e1 (op e3 e3))) (= e3 (op e4 e2))) (= e4 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e2 (op e5 e5))) (= e1 (op e4 e4))) (= e4 (op e3 e2))) (= e3 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e5 e5))) (= e3 (op e1 e1))) (= e1 (op e4 e2))) (= e4 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e2 (op e5 e5))) (= e3 (op e4 e4))) (= e4 (op e1 e2))) (= e1 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e5 e5))) (= e4 (op e1 e1))) (= e1 (op e3 e2))) (= e3 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e2 (op e5 e5))) (= e4 (op e3 e3))) (= e3 (op e1 e2))) (= e1 (op e2 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e5 e5))) (= e1 (op e2 e2))) (= e2 (op e4 e3))) (= e4 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e3 (op e5 e5))) (= e1 (op e4 e4))) (= e4 (op e2 e3))) (= e2 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e5 e5))) (= e2 (op e1 e1))) (= e1 (op e4 e3))) (= e4 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e3 (op e5 e5))) (= e2 (op e4 e4))) (= e4 (op e1 e3))) (= e1 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e5 e5))) (= e4 (op e1 e1))) (= e1 (op e2 e3))) (= e2 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e3 (op e5 e5))) (= e4 (op e2 e2))) (= e2 (op e1 e3))) (= e1 (op e3 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e5 e5))) (= e1 (op e2 e2))) (= e2 (op e3 e4))) (= e3 (op e4 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e4 (op e5 e5))) (= e1 (op e3 e3))) (= e3 (op e2 e4))) (= e2 (op e4 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e5 e5))) (= e2 (op e1 e1))) (= e1 (op e3 e4))) (= e3 (op e4 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e4 (op e5 e5))) (= e2 (op e3 e3))) (= e3 (op e1 e4))) (= e1 (op e4 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e5 e5))) (= e3 (op e1 e1))) (= e1 (op e2 e4))) (= e2 (op e4 e5)))))
+(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e4 (op e5 e5))) (= e3 (op e2 e2))) (= e2 (op e1 e4))) (= e1 (op e4 e5)))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/uf/mkpidgeon b/test/regress/regress0/uf/mkpidgeon
new file mode 100755
index 000000000..6852145ac
--- /dev/null
+++ b/test/regress/regress0/uf/mkpidgeon
@@ -0,0 +1,44 @@
+#!/bin/bash
+# Simple pidgeon-hole problem generator in SMT-LIBv2
+# (c) 2011 Morgan Deters <mdeters@cs.nyu.edu>
+# 2011 July 7
+
+if [ $# -ne 1 ]; then
+  echo "usage: $(basename "$0") size" >&2
+  exit 1
+fi
+
+N=$1
+
+echo "(set-logic QF_UF)"
+echo "(declare-sort U 0)"
+
+i=1; while [ $i -le $N ]; do
+  echo "(declare-fun p_$i () U)"
+  let ++i
+done
+
+i=1; while [ $i -le $(($N-1)) ]; do
+  echo "(declare-fun h_$i () U)"
+  let ++i
+done
+
+i=1; while [ $i -le $(($N-1)) ]; do
+  j=$(($i+1)); while [ $j -le $N ]; do
+    echo "(assert (not (= p_$i p_$j)))"
+    let ++j
+  done
+  let ++i
+done
+
+i=1; while [ $i -le $N ]; do
+  echo -n "(assert (or"
+  j=1; while [ $j -le $(($N-1)) ]; do
+    echo -n " (= p_$i h_$j)"
+    let ++j
+  done
+  echo "))"
+  let ++i
+done
+
+echo "(check-sat)"