update from the master

27 files changed, 621 insertions, 322 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 07d78a6fd..40b757598 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file boolean_terms.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
@@ -137,26 +137,6 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
   TypeNode in_t = in.getType();
   if( processing.find( in_t )==processing.end() ){
     processing[in_t] = true;
-    if(in.getType().isRecord()) {
-      Assert(as.isRecord());
-      const Record& inRec = in.getType().getRecord();
-      const Record& asRec = as.getRecord();
-      Assert(inRec.getNumFields() == asRec.getNumFields());
-      const Datatype & dt = ((DatatypeType)in.getType().toType()).getDatatype();
-      NodeBuilder<> nb(kind::APPLY_CONSTRUCTOR);
-      nb << NodeManager::currentNM()->mkConst(asRec);
-      for(size_t i = 0; i < asRec.getNumFields(); ++i) {
-        Assert(inRec[i].first == asRec[i].first);
-        Node arg = NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][i].getSelector(), in);
-        if(inRec[i].second != asRec[i].second) {
-          arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second), processing);
-        }
-        nb << arg;
-      }
-      Node out = nb;
-      processing.erase( in_t );
-      return out;
-    }
     if(in.getType().isDatatype()) {
       if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
         processing.erase( in_t );
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index e1865f29f..0a63f7fd8 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file boolean_terms.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index d6ec0769a..bd514e2a8 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file command.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Francois Bobot
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Implementation of command objects.
  **
@@ -376,6 +376,59 @@ std::string QueryCommand::getCommandName() const throw() {
   return "query";
 }
 
+
+/* class CheckSynthCommand */
+
+CheckSynthCommand::CheckSynthCommand() throw() :
+  d_expr() {
+}
+
+CheckSynthCommand::CheckSynthCommand(const Expr& expr, bool inUnsatCore) throw() :
+  d_expr(expr), d_inUnsatCore(inUnsatCore) {
+}
+
+Expr CheckSynthCommand::getExpr() const throw() {
+  return d_expr;
+}
+
+void CheckSynthCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->checkSynth(d_expr);
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Result CheckSynthCommand::getResult() const throw() {
+  return d_result;
+}
+
+void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out, verbosity);
+  } else {
+    out << d_result << endl;
+  }
+}
+
+Command* CheckSynthCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+  c->d_result = d_result;
+  return c;
+}
+
+Command* CheckSynthCommand::clone() const {
+  CheckSynthCommand* c = new CheckSynthCommand(d_expr, d_inUnsatCore);
+  c->d_result = d_result;
+  return c;
+}
+
+std::string CheckSynthCommand::getCommandName() const throw() {
+  return "check-synth";
+}
+
+
 /* class ResetCommand */
 
 void ResetCommand::invoke(SmtEngine* smtEngine) throw() {
@@ -1233,6 +1286,60 @@ std::string GetSynthSolutionCommand::getCommandName() const throw() {
   return "get-instantiations";
 }
 
+/* class GetQuantifierEliminationCommand */
+
+GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() throw() :
+  d_expr() {
+}
+
+GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(const Expr& expr, bool doFull) throw() :
+  d_expr(expr), d_doFull(doFull) {
+}
+
+Expr GetQuantifierEliminationCommand::getExpr() const throw() {
+  return d_expr;
+}
+bool GetQuantifierEliminationCommand::getDoFull() const throw() {
+  return d_doFull;
+}
+
+void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull);
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Expr GetQuantifierEliminationCommand::getResult() const throw() {
+  return d_result;
+}
+
+void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out, verbosity);
+  } else {
+    out << d_result << endl;
+  }
+}
+
+Command* GetQuantifierEliminationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr.exportTo(exprManager, variableMap), d_doFull);
+  c->d_result = d_result;
+  return c;
+}
+
+Command* GetQuantifierEliminationCommand::clone() const {
+  GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr, d_doFull);
+  c->d_result = d_result;
+  return c;
+}
+
+std::string GetQuantifierEliminationCommand::getCommandName() const throw() {
+  return d_doFull ? "get-qe" : "get-qe-disjunct";
+}
+
 /* class GetUnsatCoreCommand */
 
 GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
diff --git a/src/smt/command.h b/src/smt/command.h
index 248e69b0e..db4efd819 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file command.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Francois Bobot
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Implementation of the command pattern on SmtEngines.
  **
@@ -501,6 +501,24 @@ public:
   std::string getCommandName() const throw();
 };/* class QueryCommand */
 
+class CVC4_PUBLIC CheckSynthCommand : public Command {
+protected:
+  Expr d_expr;
+  Result d_result;
+  bool d_inUnsatCore;
+public:
+  CheckSynthCommand() throw();
+  CheckSynthCommand(const Expr& expr, bool inUnsatCore = true) throw();
+  ~CheckSynthCommand() throw() {}
+  Expr getExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Result getResult() const throw();
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+  std::string getCommandName() const throw();
+};/* class CheckSynthCommand */
+
 // this is TRANSFORM in the CVC presentation language
 class CVC4_PUBLIC SimplifyCommand : public Command {
 protected:
@@ -624,6 +642,25 @@ public:
   std::string getCommandName() const throw();
 };/* class GetSynthSolutionCommand */
 
+class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command {
+protected:
+  Expr d_expr;
+  bool d_doFull;
+  Expr d_result;
+public:
+  GetQuantifierEliminationCommand() throw();
+  GetQuantifierEliminationCommand(const Expr& expr, bool doFull) throw();
+  ~GetQuantifierEliminationCommand() throw() {}
+  Expr getExpr() const throw();
+  bool getDoFull() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Expr getResult() const throw();
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+  std::string getCommandName() const throw();
+};/* class GetQuantifierEliminationCommand */
+
 class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
 protected:
   UnsatCore d_result;
diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp
index 2319d9539..78e5914aa 100644
--- a/src/smt/command_list.cpp
+++ b/src/smt/command_list.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file command_list.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A context-sensitive list of Commands, and their cleanup
  **
diff --git a/src/smt/command_list.h b/src/smt/command_list.h
index 47185b365..ea6b64940 100644
--- a/src/smt/command_list.h
+++ b/src/smt/command_list.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file command_list.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A context-sensitive list of Commands, and their cleanup
  **
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index 3b9ec3273..eee7b901a 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -1,20 +1,21 @@
 /*********************                                                        */
 /*! \file dump.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Dump utility classes and functions
  **
  ** Dump utility classes and functions.
  **/
-#include "smt/dump.h"
 
+#include "smt/dump.h"
+#include "lib/strtok_r.h"
 #include "base/output.h"
 
 namespace CVC4 {
diff --git a/src/smt/dump.h b/src/smt/dump.h
index a6fa899da..2abfe5408 100644
--- a/src/smt/dump.h
+++ b/src/smt/dump.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file dump.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Dump utility classes and functions
  **
diff --git a/src/smt/ite_removal.cpp b/src/smt/ite_removal.cpp
index c0c6ed02b..fcd0c3254 100644
--- a/src/smt/ite_removal.cpp
+++ b/src/smt/ite_removal.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file ite_removal.cpp
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Tim King, Morgan Deters
- ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Removal of term ITEs
  **
diff --git a/src/smt/ite_removal.h b/src/smt/ite_removal.h
index d6d820f89..c0a46c316 100644
--- a/src/smt/ite_removal.h
+++ b/src/smt/ite_removal.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file ite_removal.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters
- ** Minor contributors (to current version): Clark Barrett
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Removal of term ITEs
  **
diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h
index a641f8d21..93db29a9b 100644
--- a/src/smt/logic_exception.h
+++ b/src/smt/logic_exception.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file logic_exception.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief An exception that is thrown when a feature is used outside
  ** the logic that CVC4 is currently using
diff --git a/src/smt/logic_request.cpp b/src/smt/logic_request.cpp
index 09559eb8d..dc6a2d6b7 100644
--- a/src/smt/logic_request.cpp
+++ b/src/smt/logic_request.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file logic_request.cpp
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h
index 94c6c2a5e..7b41886bd 100644
--- a/src/smt/logic_request.h
+++ b/src/smt/logic_request.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file logic_request.h
  ** \verbatim
- ** Original author: Martin Brain <>
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ **   Martin Brain, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief An object to request logic widening in the running SmtEngine
  **
diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp
index 1901f731d..cae6ac67f 100644
--- a/src/smt/managed_ostreams.cpp
+++ b/src/smt/managed_ostreams.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file managed_ostreams.cpp
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Wrappers to handle memory management of ostreams.
  **
diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h
index 6dc785027..56c517a87 100644
--- a/src/smt/managed_ostreams.h
+++ b/src/smt/managed_ostreams.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file managed_ostreams.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Wrappers to handle memory management of ostreams.
  **
diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index 15ecbadfb..a38862307 100644
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file model.cpp
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief implementation of Model class
  **/
diff --git a/src/smt/model.h b/src/smt/model.h
index 4bbcb5f7d..768cb3e6a 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file model.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Model class
  **/
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index aa645954b..369c5d48f 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file model_postprocessor.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief
  **
diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h
index 024f4f3a3..d9e749677 100644
--- a/src/smt/model_postprocessor.h
+++ b/src/smt/model_postprocessor.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file model_postprocessor.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief 
  **
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 007c5e049..5bd1cbdfc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file smt_engine.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): Christopher L. Conway, Tianyi Liang, Martin Brain <>, Kshitij Bansal, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Clark Barrett, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief The main entry point into the CVC4 library's SMT interface
  **
@@ -110,9 +110,18 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 
 namespace CVC4 {
-
 namespace smt {
 
+struct DeleteCommandFunction : public std::unary_function<const Command*, void>
+{
+  void operator()(const Command* command) { delete command; }
+};
+
+void DeleteAndClearCommandVector(std::vector<Command*>& commands) {
+  std::for_each(commands.begin(), commands.end(), DeleteCommandFunction());
+  commands.clear();
+}
+
 /** Useful for counting the number of recursive calls. */
 class ScopeCounter {
 private:
@@ -543,6 +552,11 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   unsigned d_simplifyAssertionsDepth;
 
+  /** whether certain preprocess steps are necessary */
+  bool d_needsExpandDefs;
+  bool d_needsRewriteBoolTerms;
+  bool d_needsConstrainSubTypes;
+
 public:
   /**
    * Map from skolem variables to index in d_assertions containing
@@ -670,6 +684,9 @@ public:
     d_abstractValueMap(&d_fakeContext),
     d_abstractValues(),
     d_simplifyAssertionsDepth(0),
+    d_needsExpandDefs(true),
+    d_needsRewriteBoolTerms(true),
+    d_needsConstrainSubTypes(true), //TODO
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
     d_pbsProcessor(smt.d_userContext),
@@ -955,6 +972,45 @@ public:
   std::ostream* getReplayLog() const {
     return d_managedReplayLog.getReplayLog();
   }
+
+  Node replaceQuantifiersWithInstantiations( Node n, std::map< Node, std::vector< Node > >& insts, std::map< Node, Node >& visited ){
+    std::map< Node, Node >::iterator itv = visited.find( n );
+    if( itv!=visited.end() ){
+      return itv->second;
+    }else{
+      Node ret = n;
+      if( n.getKind()==kind::FORALL ){
+        std::map< Node, std::vector< Node > >::iterator it = insts.find( n );
+        if( it==insts.end() ){
+          Trace("smt-qe-debug") << "* " << n << " has no instances" << std::endl;
+          ret = NodeManager::currentNM()->mkConst(true);
+        }else{
+          Trace("smt-qe-debug") << "* " << n << " has " << it->second.size() << " instances" << std::endl;
+          Node reti = it->second.empty() ? NodeManager::currentNM()->mkConst(true) : ( it->second.size()==1 ? it->second[0] : NodeManager::currentNM()->mkNode( kind::AND, it->second ) );
+          Trace("smt-qe-debug") << "   return : " << ret << std::endl;
+          //recursive (for nested quantification)
+          ret = replaceQuantifiersWithInstantiations( reti, insts, visited );
+        }     
+      }else if( n.getNumChildren()>0 ){
+        bool childChanged = false;
+        std::vector< Node > children;
+        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.push_back( n.getOperator() );
+        }
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          Node r = replaceQuantifiersWithInstantiations( n[i], insts, visited );
+          children.push_back( r );
+          childChanged = childChanged || r!=n[i];
+        }
+        if( childChanged ){
+          ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+        }
+      }
+      visited[n] = ret;
+      return ret;
+    }
+  }
+
 };/* class SmtEnginePrivate */
 
 }/* namespace CVC4::smt */
@@ -1007,7 +1063,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
   // initialized in TheoryEngine and PropEngine respectively. 
   Assert(d_proofManager == NULL);
-  PROOF( d_proofManager = new ProofManager(); ); 
+#ifdef CVC4_PROOF
+  d_proofManager = new ProofManager();
+#endif
   
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
@@ -1039,20 +1097,27 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
 }
 
 void SmtEngine::finishInit() {
+  Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
   // ensure that our heuristics are properly set up
   setDefaults();
+  
+  Trace("smt-debug") << "Making decision engine..." << std::endl;
 
   d_decisionEngine = new DecisionEngine(d_context, d_userContext);
   d_decisionEngine->init();   // enable appropriate strategies
 
+  Trace("smt-debug") << "Making prop engine..." << std::endl;
   d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context,
                                 d_userContext, d_private->getReplayLog(),
                                 d_replayStream, d_channels);
 
+  Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(d_propEngine);
   d_theoryEngine->setDecisionEngine(d_decisionEngine);
+  Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
   d_theoryEngine->finishInit();
 
+  Trace("smt-debug") << "Set up assertion list..." << std::endl;
   // [MGD 10/20/2011] keep around in incremental mode, due to a
   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
   // first, some user-context-dependent TNodes might still exist
@@ -1073,6 +1138,7 @@ void SmtEngine::finishInit() {
                       << SetBenchmarkLogicCommand(everything.getLogicString());
   }
 
+  Trace("smt-debug") << "Dump declaration commands..." << std::endl;
   // dump out any pending declaration commands
   for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
     Dump("declarations") << *d_dumpCommands[i];
@@ -1081,6 +1147,7 @@ void SmtEngine::finishInit() {
   d_dumpCommands.clear();
 
   PROOF( ProofManager::currentPM()->setLogic(d_logic); );
+  Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
 }
 
 void SmtEngine::finalOptionsAreSet() {
@@ -1155,6 +1222,8 @@ SmtEngine::~SmtEngine() throw() {
     }
     d_dumpCommands.clear();
 
+    DeleteAndClearCommandVector(d_modelGlobalCommands);
+
     if(d_modelCommands != NULL) {
       d_modelCommands->deleteSelf();
     }
@@ -1260,15 +1329,7 @@ void SmtEngine::setDefaults() {
       Trace("smt") << "turning on quantifier logic, for strings-exp"
                    << std::endl;
     }
-    if(! options::finiteModelFind.wasSetByUser()) {
-      options::finiteModelFind.set( true );
-      Trace("smt") << "turning on finite-model-find, for strings-exp"
-                   << std::endl;
-    }
     if(! options::fmfBoundInt.wasSetByUser()) {
-      if(! options::fmfBoundIntLazy.wasSetByUser()) {
-        options::fmfBoundIntLazy.set( true );
-      }
       options::fmfBoundInt.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
@@ -1644,16 +1705,25 @@ void SmtEngine::setDefaults() {
     options::sortInference.set( false );
     options::ufssFairnessMonotone.set( false );
   }
+  if( d_logic.hasCardinalityConstraints() ){
+    //must have finite model finding on
+    options::finiteModelFind.set( true );
+  }
+  
+  //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
+  if( d_logic.isTheoryEnabled(THEORY_STRINGS) || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ){
+    if( !options::instWhenStrictInterleave.wasSetByUser() ){
+      options::instWhenStrictInterleave.set( false );
+    }
+  }
+  
   //local theory extensions
   if( options::localTheoryExt() ){
     if( !options::instMaxLevel.wasSetByUser() ){
       options::instMaxLevel.set( 0 );
     }
   }
-  if( d_logic.hasCardinalityConstraints() ){
-    //must have finite model finding on
-    options::finiteModelFind.set( true );
-  }
+
   if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) {
     options::fmfBoundInt.set( true );
   }
@@ -1752,26 +1822,25 @@ void SmtEngine::setDefaults() {
     if( !options::cbqiPreRegInst.wasSetByUser()) {
       options::cbqiPreRegInst.set( true );
     }
-  }else{
-    //counterexample-guided instantiation for non-sygus
-    // enable if any quantifiers with arithmetic or datatypes
-    if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || 
-        options::cbqiAll() ){
-      if( !options::cbqi.wasSetByUser() ){
-        options::cbqi.set( true );
-      }
-    }
-    if( options::cbqiSplx() ){
-      //implies more general option
+  }
+  //counterexample-guided instantiation for non-sygus
+  // enable if any quantifiers with arithmetic or datatypes
+  if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || 
+      options::cbqiAll() ){
+    if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );
     }
-    if( options::cbqi() ){
-      //must rewrite divk
-      if( !options::rewriteDivk.wasSetByUser()) {
-        options::rewriteDivk.set( true );
-      }
+  }
+  if( options::cbqiSplx() ){
+    //implies more general option
+    options::cbqi.set( true );
+  }
+  if( options::cbqi() ){
+    //must rewrite divk
+    if( !options::rewriteDivk.wasSetByUser()) {
+      options::rewriteDivk.set( true );
     }
-    if( options::cbqi() && d_logic.isPure(THEORY_ARITH) ){
+    if( d_logic.isPure(THEORY_ARITH) ){
       options::cbqiAll.set( false );
       if( !options::quantConflictFind.wasSetByUser() ){
         options::quantConflictFind.set( false );
@@ -1787,8 +1856,12 @@ void SmtEngine::setDefaults() {
       }
     }
   }
-
   //implied options...
+  if( options::strictTriggers() ){
+    if( !options::userPatternsQuant.wasSetByUser() ){
+      options::userPatternsQuant.set( quantifiers::USER_PAT_MODE_TRUST );
+    }
+  }
   if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
     options::quantConflictFind.set( true );
   }
@@ -1843,6 +1916,9 @@ void SmtEngine::setDefaults() {
       options::preSkolemQuantNested.set( false );
     }
   }
+  if( !d_logic.isTheoryEnabled(THEORY_DATATYPES) ){
+    options::quantDynamicSplit.set( quantifiers::QUANT_DSPLIT_MODE_NONE );
+  }
 
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
@@ -2063,6 +2139,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
 void SmtEngine::defineFunction(Expr func,
                                const std::vector<Expr>& formals,
                                Expr formula) {
+  SmtScope smts(this);
+  doPendingPops();
   Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
   for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) {
     if((*i).getKind() != kind::BOUND_VARIABLE) {
@@ -2081,7 +2159,6 @@ void SmtEngine::defineFunction(Expr func,
   DefineFunctionCommand c(ss.str(), func, formals, formula);
   addToModelCommandAndDump(c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
 
-  SmtScope smts(this);
 
   PROOF( if (options::checkUnsatCores()) {
       d_defineCommands.push_back(c.clone());
@@ -3572,6 +3649,7 @@ Result SmtEngine::check() {
   // Make sure the prop layer has all of the assertions
   Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
   d_private->processAssertions();
+  Trace("smt") << "SmtEngine::check(): done processing assertions" << endl;
 
   // Turn off stop only for QF_LRA
   // TODO: Bring up in a meeting where to put this
@@ -3807,6 +3885,7 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
+
   dumpAssertions("pre-constrain-subtypes", d_assertions);
   {
     // Any variables of subtype types need to be constrained properly.
@@ -4141,6 +4220,7 @@ void SmtEnginePrivate::processAssertions() {
 
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
   dumpAssertions("post-everything", d_assertions);
+  
 
   //set instantiation level of everything to zero
   if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
@@ -4210,13 +4290,22 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
 }
 
 Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
+  return checkSatisfiability( ex, inUnsatCore, false );
+}/* SmtEngine::checkSat() */
+
+Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
+  Assert(!ex.isNull());
+  return checkSatisfiability( ex, inUnsatCore, true );
+}/* SmtEngine::query() */
+
+Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQuery) {
   try {
     Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
     SmtScope smts(this);
     finalOptionsAreSet();
     doPendingPops();
 
-    Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl;
+    Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" << ex << ")" << endl;
 
     if(d_queryMade && !options::incrementalSolving()) {
       throw ModalException("Cannot make multiple queries unless "
@@ -4247,14 +4336,15 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
     // Add the formula
     if(!e.isNull()) {
       d_problemExtended = true;
+      Expr ea = isQuery ? e.notExpr() : e;
       if(d_assertionList != NULL) {
-        d_assertionList->push_back(e);
+        d_assertionList->push_back(ea);
       }
-      d_private->addFormula(e.getNode(), inUnsatCore);
+      d_private->addFormula(ea.getNode(), inUnsatCore);
     }
 
     Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
-    r = check().asSatisfiabilityResult();
+    r = isQuery ? check().asValidityResult() : check().asSatisfiabilityResult();
 
     if (options::solveIntAsBV() > 0 &&r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
       r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
@@ -4265,7 +4355,11 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
     // Dump the query if requested
     if(Dump.isOn("benchmark")) {
       // the expr already got dumped out if assertion-dumping is on
-      Dump("benchmark") << CheckSatCommand(ex);
+      if( isQuery ){
+        Dump("benchmark") << QueryCommand(ex);
+      }else{
+        Dump("benchmark") << CheckSatCommand(ex);
+      }
     }
 
     // Pop the context
@@ -4276,7 +4370,7 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
 
     d_problemExtended = false;
 
-    Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
+    Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" << e << ") => " << r << endl;
 
     // Check that SAT results generate a model correctly.
     if(options::checkModels()) {
@@ -4307,98 +4401,85 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
       Result::RESOURCEOUT : Result::TIMEOUT;
     return Result(Result::SAT_UNKNOWN, why, d_filename);
   }
-}/* SmtEngine::checkSat() */
-
-Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
-  Assert(!ex.isNull());
-  Assert(ex.getExprManager() == d_exprManager);
-  SmtScope smts(this);
-  finalOptionsAreSet();
-  doPendingPops();
-  Trace("smt") << "SMT query(" << ex << ")" << endl;
-
-  try {
-  if(d_queryMade && !options::incrementalSolving()) {
-    throw ModalException("Cannot make multiple queries unless "
-                         "incremental solving is enabled "
-                         "(try --incremental)");
-  }
-
-  // Substitute out any abstract values in ex
-  Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
-  // Ensure that the expression is type-checked at this point, and Boolean
-  ensureBoolean(e);
-
-  // check to see if a postsolve() is pending
-  if(d_needPostsolve) {
-    d_theoryEngine->postsolve();
-    d_needPostsolve = false;
-  }
-
-  // Push the context
-  internalPush();
-
-  // Note that a query has been made
-  d_queryMade = true;
-
-  // Add the formula
-  d_problemExtended = true;
-  if(d_assertionList != NULL) {
-    d_assertionList->push_back(e.notExpr());
-  }
-  d_private->addFormula(e.getNode().notNode(), inUnsatCore);
-
-  // Run the check
-  Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
-  r = check().asValidityResult();
-  d_needPostsolve = true;
-
-  // Dump the query if requested
-  if(Dump.isOn("benchmark")) {
-    // the expr already got dumped out if assertion-dumping is on
-    Dump("benchmark") << QueryCommand(ex);
-  }
-
-  // Pop the context
-  internalPop();
-
-  // Remember the status
-  d_status = r;
-
-  d_problemExtended = false;
+}
 
-  Trace("smt") << "SMT query(" << e << ") ==> " << r << endl;
 
-  // Check that SAT results generate a model correctly.
-  if(options::checkModels()) {
-    if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
-       (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
-      checkModel(/* hard failure iff */ ! r.isUnknown());
-    }
-  }
-  // Check that UNSAT results generate a proof correctly.
-  if(options::checkProofs()) {
-    if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
-      TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
-      checkProof();
-    }
-  }
-  // Check that UNSAT results generate an unsat core correctly.
-  if(options::checkUnsatCores()) {
-    if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
-      TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
-      checkUnsatCore();
+Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalException, LogicException) {
+  SmtScope smts(this);
+  Trace("smt") << "Check synth: " << e << std::endl;
+  Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl;
+  Expr e_check = e;
+  Node conj = Node::fromExpr( e );
+  Assert( conj.getKind()==kind::FORALL );
+  //possibly run quantifier elimination to make formula into single invocation
+  if( conj[1].getKind()==kind::EXISTS ){
+    Node conj_se = conj[1][1];
+    
+    Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl;
+    quantifiers::SingleInvocationPartition sip( kind::APPLY );
+    sip.init( conj_se );
+    Trace("smt-synth") << "...finished, got:" << std::endl;
+    sip.debugPrint("smt-synth");
+    
+    if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){
+      //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f.
+      //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), 
+      //  and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f.  We invoke synthesis solver on this result.
+    
+      //create new smt engine to do quantifier elimination
+      SmtEngine smt_qe( d_exprManager );
+      smt_qe.setLogic(getLogicInfo());
+      Trace("smt-synth") << "Property is non-ground single invocation, run QE to obtain single invocation." << std::endl;
+      //partition variables
+      std::vector< Node > qe_vars;
+      std::vector< Node > nqe_vars;
+      for( unsigned i=0; i<sip.d_all_vars.size(); i++ ){
+        Node v = sip.d_all_vars[i];
+        if( std::find( sip.d_si_vars.begin(), sip.d_si_vars.end(), v )==sip.d_si_vars.end() ){
+          qe_vars.push_back( v );
+        }else{
+          nqe_vars.push_back( v );
+        }
+      }
+      std::vector< Node > orig;
+      std::vector< Node > subs;
+      //skolemize non-qe variables
+      for( unsigned i=0; i<nqe_vars.size(); i++ ){
+        Node k = NodeManager::currentNM()->mkSkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation" );
+        orig.push_back( nqe_vars[i] );
+        subs.push_back( k );
+        Trace("smt-synth") << "  subs : " << nqe_vars[i] << " -> " << k << std::endl;
+      }
+      for( std::map< Node, bool >::iterator it = sip.d_funcs.begin(); it != sip.d_funcs.end(); ++it ){
+        orig.push_back( sip.d_func_inv[it->first] );
+        Node k = NodeManager::currentNM()->mkSkolem( "k", sip.d_func_fo_var[it->first].getType(), "qe for function in non-ground single invocation" );
+        subs.push_back( k );
+        Trace("smt-synth") << "  subs : " << sip.d_func_inv[it->first] << " -> " << k << std::endl;
+      }
+      Node conj_se_ngsi = sip.getFullSpecification();
+      Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() );
+      Assert( !qe_vars.empty() );
+      conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs );
+      
+      Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl;
+      Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false );
+      Trace("smt-synth") << "Result : " << qe_res << std::endl;
+      
+      //create single invocation conjecture
+      Node qe_res_n = Node::fromExpr( qe_res );
+      qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() );
+      if( !nqe_vars.empty() ){
+        qe_res_n = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, nqe_vars ), qe_res_n );
+      }
+      Assert( conj.getNumChildren()==3 );
+      qe_res_n = NodeManager::currentNM()->mkNode( kind::FORALL, conj[0], qe_res_n, conj[2] );
+      Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n << std::endl;
+      e_check = qe_res_n.toExpr();
     }
   }
-
-  return r;
-  } catch (UnsafeInterruptException& e) {
-    AlwaysAssert(d_private->getResourceManager()->out());
-    Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ?
-      Result::RESOURCEOUT : Result::TIMEOUT;
-    return Result(Result::VALIDITY_UNKNOWN, why, d_filename);
-  }
-}/* SmtEngine::query() */
+  
+  return checkSatisfiability( e_check, true, false );
+}
 
 Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
   Assert(ex.getExprManager() == d_exprManager);
@@ -5017,6 +5098,77 @@ void SmtEngine::printSynthSolution( std::ostream& out ) {
   }
 }
 
+Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) throw(TypeCheckingException, ModalException, LogicException) {
+  SmtScope smts(this);
+  if(!d_logic.isPure(THEORY_ARITH) && strict){
+    Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
+  }
+  Trace("smt-qe") << "Do quantifier elimination " << e << std::endl;
+  Node n_e = Node::fromExpr( e );  
+  if( n_e.getKind()!=kind::EXISTS ){
+    throw ModalException("Expecting an existentially quantified formula as argument to get-qe.");
+  }
+  //tag the quantified formula with the quant-elim attribute
+  TypeNode t = NodeManager::currentNM()->booleanType();
+  Node n_attr = NodeManager::currentNM()->mkSkolem("qe", t, "Auxiliary variable for qe attr.");
+  std::vector< Node > node_values;
+  d_theoryEngine->setUserAttribute( doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
+  n_attr = NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE, n_attr);
+  n_attr = NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST, n_attr);
+  std::vector< Node > e_children;
+  e_children.push_back( n_e[0] );
+  e_children.push_back( n_e[1] );
+  e_children.push_back( n_attr );
+  Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children );
+  Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e << std::endl;
+  Assert( nn_e.getNumChildren()==3 );
+  Result r = checkSatisfiability(nn_e.toExpr(), true, true);
+  Trace("smt-qe") << "Query returned " << r << std::endl;
+  if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) {
+    if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){
+      stringstream ss;
+      ss << "While performing quantifier elimination, unexpected result : " << r << " for query.";
+      InternalError(ss.str().c_str());
+    }
+    //get the instantiations for all quantified formulas
+    std::map< Node, std::vector< Node > > insts;    
+    d_theoryEngine->getInstantiations( insts );
+    //find the quantified formula that corresponds to the input
+    Node top_q;
+    for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){
+      Trace("smt-qe-debug") << "* quantifier " << it->first << " had " << it->second.size() << " instances." << std::endl;
+      if( it->first.getNumChildren()==3 && it->first[2]==n_attr ){
+        top_q = it->first;
+      }
+    }
+    std::map< Node, Node > visited;
+    Node ret_n;
+    if( top_q.isNull() ){
+      //no instances needed
+      ret_n = NodeManager::currentNM()->mkConst(true);
+      visited[top_q] = ret_n;
+    }else{
+      //replace by a conjunction of instances
+      ret_n = d_private->replaceQuantifiersWithInstantiations( top_q, insts, visited );
+    }
+
+    //ensure all instantiations were accounted for
+    for( std::map< Node, std::vector< Node > >::iterator it = insts.begin(); it != insts.end(); ++it ){
+      if( !it->second.empty() && visited.find( it->first )==visited.end() ){
+        stringstream ss;
+        ss << "While performing quantifier elimination, processed a quantified formula : " << it->first;
+        ss << " that was not related to the query.  Try option --simplification=none.";
+        InternalError(ss.str().c_str());
+      }
+    }
+    Trace("smt-qe") << "Returned : " << ret_n << std::endl;
+    ret_n = Rewriter::rewrite( ret_n.negate() );
+    return ret_n.toExpr();
+  }else {
+    return NodeManager::currentNM()->mkConst(true).toExpr();
+  }
+}
+
 vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -5174,7 +5326,7 @@ void SmtEngine::resetAssertions() throw() {
   Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
   d_context->popto(0);
   d_userContext->popto(0);
-  d_modelGlobalCommands.clear();
+  DeleteAndClearCommandVector(d_modelGlobalCommands);
   d_userContext->push();
   d_context->push();
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3616762bc..2741cea85 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file smt_engine.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Martin Brain <>, Tim King, Clark Barrett, Christopher L. Conway, Andrew Reynolds, Kshitij Bansal, Dejan Jovanovic
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief SmtEngine: the main public entry point of libcvc4.
  **
@@ -244,11 +244,11 @@ class CVC4_PUBLIC SmtEngine {
   bool d_needPostsolve;
 
   /*
-   * Whether to call theory preprocessing during simplification - on by default* but gets turned off if arithRewriteEq is on
+   * Whether to call theory preprocessing during simplification - on
+   * by default* but gets turned off if arithRewriteEq is on
    */
   bool d_earlyTheoryPP;
 
-
   /**
    * Most recent result of last checkSat/query or (set-info :status).
    */
@@ -401,6 +401,8 @@ class CVC4_PUBLIC SmtEngine {
   SmtEngine(const SmtEngine&) CVC4_UNDEFINED;
   SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED;
 
+  //check satisfiability (for query and check-sat)
+  Result checkSatisfiability(const Expr& e, bool inUnsatCore, bool isQuery);
 public:
 
   /**
@@ -494,6 +496,12 @@ public:
   Result checkSat(const Expr& e = Expr(), bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException);
 
   /**
+   * Assert a synthesis conjecture to the current context and call
+   * check().  Returns sat, unsat, or unknown result.
+   */
+  Result checkSynth(const Expr& e) throw(TypeCheckingException, ModalException, LogicException);
+
+  /**
    * Simplify a formula without doing "much" work.  Does not involve
    * the SAT Engine in the simplification, but uses the current
    * definitions, assertions, and the current partial model, if one
@@ -553,6 +561,11 @@ public:
   void printSynthSolution( std::ostream& out );
 
   /**
+   * Do quantifier elimination, doFull false means just output one disjunct, strict is whether to output warnings.
+   */
+  Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict=true) throw(TypeCheckingException, ModalException, LogicException);
+
+  /**
    * Get an unsatisfiable core (only if immediately preceded by an
    * UNSAT or VALID query).  Only permitted if CVC4 was built with
    * unsat-core support and produce-unsat-cores is on.
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index 354a43cc8..5634a4651 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file smt_engine_check_proof.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Guy Katz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
@@ -22,7 +22,7 @@
 #include <fstream>
 #include <string>
 
-#warning "TODO: Why is lfsc's check.h being included like this?"
+// #warning "TODO: Why is lfsc's check.h being included like this?"
 #include "check.h"
 
 #include "base/configuration_private.h"
@@ -63,17 +63,26 @@ void SmtEngine::checkProof() {
 
   Chat() << "checking proof..." << endl;
 
-  if( !(d_logic.isPure(theory::THEORY_BOOL) ||
-        d_logic.isPure(theory::THEORY_BV) ||
-	(d_logic.isPure(theory::THEORY_UF) &&
-	 ! d_logic.hasCardinalityConstraints())) ||
-      d_logic.isQuantified()) {
+  if ( !(d_logic.isPure(theory::THEORY_BOOL) ||
+           d_logic.isPure(theory::THEORY_BV) ||
+           d_logic.isPure(theory::THEORY_ARRAY) ||
+           (d_logic.isPure(theory::THEORY_UF) &&
+            ! d_logic.hasCardinalityConstraints())) ||
+       d_logic.isQuantified()) {
     // no checking for these yet
     Notice() << "Notice: no proof-checking for non-UF/Bool/BV proofs yet" << endl;
     return;
   }
 
-  char* pfFile = strdup("/tmp/cvc4_proof.XXXXXX");
+  char const* tempDir = getenv("TMPDIR");
+  if (!tempDir) {
+    tempDir = "/tmp";
+  }
+
+  stringstream pfPath;
+  pfPath << tempDir << "/cvc4_proof.XXXXXX";
+
+  char* pfFile = strdup(pfPath.str().c_str());
   int fd = mkstemp(pfFile);
 
   // ensure this temp file is removed after
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 25004c85e..c31ea5736 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file smt_engine_scope.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 5a7e39849..e00be40d4 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file smt_engine_scope.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp
index 5aa9085f5..d34498697 100644
--- a/src/smt/smt_statistics_registry.cpp
+++ b/src/smt/smt_statistics_registry.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
-/*! \file smt_statistic_registry.cpp
+/*! \file smt_statistics_registry.cpp
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Accessor for the SmtEngine's StatisticsRegistry.
  **
diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h
index 60a5e7c53..7483e8215 100644
--- a/src/smt/smt_statistics_registry.h
+++ b/src/smt/smt_statistics_registry.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
-/*! \file smt_statistic_registry.h
+/*! \file smt_statistics_registry.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Accessor for the SmtEngine's StatisticsRegistry.
  **
diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h
index b87ed69d2..9574c5460 100644
--- a/src/smt/update_ostream.h
+++ b/src/smt/update_ostream.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file update_ostream.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **