Merge branch 'master' into lfscTestslfscTests

70 files changed, 232 insertions, 295 deletions

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 7408f4ba3..caad369b7 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andres Noetzli, Justin Xu, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index b133bc490..5d8f64594 100644
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andres Noetzli, Justin Xu, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index 888456174..31c92a09f 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -2,9 +2,9 @@
 /*! \file ackermann.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar, Aina Niemetz, Clark Barrett, Ying Sheng
+ **   Ying Sheng, Yoni Zohar, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h
index 4aa26da85..1d2b6e9ce 100644
--- a/src/preprocessing/passes/ackermann.h
+++ b/src/preprocessing/passes/ackermann.h
@@ -2,9 +2,9 @@
 /*! \file ackermann.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Yoni Zohar
+ **   Ying Sheng, Aina Niemetz, Yoni Zohar
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 98313efda..71aa028d4 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -2,9 +2,9 @@
 /*! \file apply_substs.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Andres Noetzli
+ **   Aina Niemetz, Andres Noetzli, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h
index f20ffa61e..4f2dd24e5 100644
--- a/src/preprocessing/passes/apply_substs.h
+++ b/src/preprocessing/passes/apply_substs.h
@@ -2,9 +2,9 @@
 /*! \file apply_substs.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz
+ **   Aina Niemetz, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index e18e6f6c6..ad512bdfd 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Makai Mann, Yoni Zohar, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h
index 6e6d368eb..968672e86 100644
--- a/src/preprocessing/passes/bool_to_bv.h
+++ b/src/preprocessing/passes/bool_to_bv.h
@@ -2,9 +2,9 @@
 /*! \file bool_to_bv.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar, Makai Mann, Liana Hadarean
+ **   Makai Mann, Yoni Zohar, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp
index d62c8a97e..5d6ed9b4f 100644
--- a/src/preprocessing/passes/bv_abstraction.cpp
+++ b/src/preprocessing/passes/bv_abstraction.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h
index b5840b355..aa1134a9b 100644
--- a/src/preprocessing/passes/bv_abstraction.h
+++ b/src/preprocessing/passes/bv_abstraction.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp
index a16a8347d..d4dd2b9b9 100644
--- a/src/preprocessing/passes/bv_eager_atoms.cpp
+++ b/src/preprocessing/passes/bv_eager_atoms.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h
index 4ed685855..cd84f1aaa 100644
--- a/src/preprocessing/passes/bv_eager_atoms.h
+++ b/src/preprocessing/passes/bv_eager_atoms.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index b08f69b50..68696015e 100644
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -2,9 +2,9 @@
 /*! \file bv_gauss.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Tim King
+ **   Aina Niemetz, Mathias Preiner, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h
index 7fb23814a..f09b2dbe4 100644
--- a/src/preprocessing/passes/bv_gauss.h
+++ b/src/preprocessing/passes/bv_gauss.h
@@ -2,9 +2,9 @@
 /*! \file bv_gauss.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz
+ **   Aina Niemetz, Mathias Preiner, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp
index bfc02f332..a0f2ffdd5 100644
--- a/src/preprocessing/passes/bv_intro_pow2.cpp
+++ b/src/preprocessing/passes/bv_intro_pow2.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Mathias Preiner, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h
index 86d5ebfef..fcfef6f39 100644
--- a/src/preprocessing/passes/bv_intro_pow2.h
+++ b/src/preprocessing/passes/bv_intro_pow2.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index 33b41210a..f4d4d5b8c 100644
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Yoni Zohar, Liana Hadarean, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h
index dc0494943..f0f4b3856 100644
--- a/src/preprocessing/passes/bv_to_bool.h
+++ b/src/preprocessing/passes/bv_to_bool.h
@@ -2,9 +2,9 @@
 /*! \file bv_to_bool.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Yoni Zohar, Tim King
+ **   Liana Hadarean, Yoni Zohar, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 0e4bc41c0..5b125b4b6 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -2,9 +2,9 @@
 /*! \file bv_to_int.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar and Ahmed Irfan
+ **   Yoni Zohar, Ahmed Irfan
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
@@ -184,43 +184,41 @@ Node BVToInt::eliminationPass(Node n)
         (d_eliminationCache.find(current) != d_eliminationCache.end());
     bool inRebuildCache =
         (d_rebuildCache.find(current) != d_rebuildCache.end());
-    if (!inRebuildCache)
+    if (!inEliminationCache)
     {
-      // current is not the elimination of any previously-visited node
-      if (!inEliminationCache)
-      {
-        // current hasn't been eliminated yet.
-        // eliminate operators from it
-        Node currentEliminated =
-            FixpointRewriteStrategy<RewriteRule<UdivZero>,
-                                    RewriteRule<SdivEliminate>,
-                                    RewriteRule<SremEliminate>,
-                                    RewriteRule<SmodEliminate>,
-                                    RewriteRule<RepeatEliminate>,
-                                    RewriteRule<ZeroExtendEliminate>,
-                                    RewriteRule<SignExtendEliminate>,
-                                    RewriteRule<RotateRightEliminate>,
-                                    RewriteRule<RotateLeftEliminate>,
-                                    RewriteRule<CompEliminate>,
-                                    RewriteRule<SleEliminate>,
-                                    RewriteRule<SltEliminate>,
-                                    RewriteRule<SgtEliminate>,
-                                    RewriteRule<SgeEliminate>,
-                                    RewriteRule<ShlByConst>,
-                                    RewriteRule<LshrByConst> >::apply(current);
-        // save in the cache
-        d_eliminationCache[current] = currentEliminated;
-        // put the eliminated node in the rebuild cache, but mark that it hasn't
-        // yet been rebuilt by assigning null.
-        d_rebuildCache[currentEliminated] = Node();
-        // Push the eliminated node to the stack
-        toVisit.push_back(currentEliminated);
-        // Add the children to the stack for future processing.
-        toVisit.insert(
-            toVisit.end(), currentEliminated.begin(), currentEliminated.end());
-      }
+      // current hasn't been eliminated yet.
+      // eliminate operators from it
+      Node currentEliminated =
+          FixpointRewriteStrategy<RewriteRule<UdivZero>,
+                                  RewriteRule<SdivEliminate>,
+                                  RewriteRule<SremEliminate>,
+                                  RewriteRule<SmodEliminate>,
+                                  RewriteRule<RepeatEliminate>,
+                                  RewriteRule<ZeroExtendEliminate>,
+                                  RewriteRule<SignExtendEliminate>,
+                                  RewriteRule<RotateRightEliminate>,
+                                  RewriteRule<RotateLeftEliminate>,
+                                  RewriteRule<CompEliminate>,
+                                  RewriteRule<SleEliminate>,
+                                  RewriteRule<SltEliminate>,
+                                  RewriteRule<SgtEliminate>,
+                                  RewriteRule<SgeEliminate>,
+                                  RewriteRule<ShlByConst>,
+                                  RewriteRule<LshrByConst> >::apply(current);
+      // save in the cache
+      d_eliminationCache[current] = currentEliminated;
+      // also assign the eliminated now to itself to avoid revisiting.
+      d_eliminationCache[currentEliminated] = currentEliminated;
+      // put the eliminated node in the rebuild cache, but mark that it hasn't
+      // yet been rebuilt by assigning null.
+      d_rebuildCache[currentEliminated] = Node();
+      // Push the eliminated node to the stack
+      toVisit.push_back(currentEliminated);
+      // Add the children to the stack for future processing.
+      toVisit.insert(
+          toVisit.end(), currentEliminated.begin(), currentEliminated.end());
     }
-    else
+    if (inRebuildCache)
     {
       // current was already added to the rebuild cache.
       if (d_rebuildCache[current].isNull())
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index f0e0ea02e..5015d1e8e 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -2,9 +2,9 @@
 /*! \file bv_to_int.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar and Ahmed Irfan
+ **   Yoni Zohar
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
index 8bf4cc816..39b3e1512 100644
--- a/src/preprocessing/passes/extended_rewriter_pass.cpp
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h
index dbaaa05ad..de6648d17 100644
--- a/src/preprocessing/passes/extended_rewriter_pass.h
+++ b/src/preprocessing/passes/extended_rewriter_pass.h
@@ -2,9 +2,9 @@
 /*! \file extended_rewriter_pass.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index 59b5ddf6e..25bb0e532 100644
--- a/src/preprocessing/passes/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Yoni Zohar
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h
index 89c3a3e3e..67cb0f770 100644
--- a/src/preprocessing/passes/global_negate.h
+++ b/src/preprocessing/passes/global_negate.h
@@ -2,9 +2,9 @@
 /*! \file global_negate.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar
+ **   Yoni Zohar, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 65945f0d7..bb524315a 100644
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h
index f0de321c4..be088c46b 100644
--- a/src/preprocessing/passes/ho_elim.h
+++ b/src/preprocessing/passes/ho_elim.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 9fa9a0c05..e30c03f26 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -2,9 +2,9 @@
 /*! \file int_to_bv.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli
+ **   Andres Noetzli, Yoni Zohar, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "expr/node_traversal.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
@@ -36,107 +37,58 @@ using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
 
 namespace {
 
-// TODO: clean this up
-struct intToBV_stack_element
-{
-  TNode d_node;
-  bool d_children_added;
-  intToBV_stack_element(TNode node) : d_node(node), d_children_added(false) {}
-}; /* struct intToBV_stack_element */
-
 bool childrenTypesChanged(Node n, NodeMap& cache) {
-  bool result = false;
   for (Node child : n) {
     TypeNode originalType = child.getType();
     TypeNode newType = cache[child].getType();
     if (! newType.isSubtypeOf(originalType)) {
-      result = true;
-      break;
+      return true;
     }
   }
-  return result;
+  return false;
 }
 
 
 Node intToBVMakeBinary(TNode n, NodeMap& cache)
 {
-  // Do a topological sort of the subexpressions and substitute them
-  vector<intToBV_stack_element> toVisit;
-  toVisit.push_back(n);
-
-  while (!toVisit.empty())
+  for (TNode current : NodeDfsIterable(n, VisitOrder::POSTORDER,
+           [&cache](TNode nn) { return cache.count(nn) > 0; }))
   {
-    // The current node we are processing
-    intToBV_stack_element& stackHead = toVisit.back();
-    TNode current = stackHead.d_node;
-
-    NodeMap::iterator find = cache.find(current);
-    if (find != cache.end())
+    Node result;
+    NodeManager* nm = NodeManager::currentNM();
+    if (current.getNumChildren() == 0)
     {
-      toVisit.pop_back();
-      continue;
+      result = current;
     }
-    if (stackHead.d_children_added)
+    else if (current.getNumChildren() > 2
+             && (current.getKind() == kind::PLUS
+                 || current.getKind() == kind::MULT))
     {
-      // Children have been processed, so rebuild this node
-      Node result;
-      NodeManager* nm = NodeManager::currentNM();
-      if (current.getNumChildren() > 2
-          && (current.getKind() == kind::PLUS
-              || current.getKind() == kind::MULT))
-      {
-        Assert(cache.find(current[0]) != cache.end());
-        result = cache[current[0]];
-        for (unsigned i = 1; i < current.getNumChildren(); ++i)
-        {
-          Assert(cache.find(current[i]) != cache.end());
-          Node child = current[i];
-          Node childRes = cache[current[i]];
-          result = nm->mkNode(current.getKind(), result, childRes);
-        }
-      }
-      else
+      Assert(cache.find(current[0]) != cache.end());
+      result = cache[current[0]];
+      for (unsigned i = 1; i < current.getNumChildren(); ++i)
       {
-        NodeBuilder<> builder(current.getKind());
-        if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
-          builder << current.getOperator();
-        }
-
-        for (unsigned i = 0; i < current.getNumChildren(); ++i)
-        {
-          Assert(cache.find(current[i]) != cache.end());
-          builder << cache[current[i]];
-        }
-        result = builder;
+        Assert(cache.find(current[i]) != cache.end());
+        Node child = current[i];
+        Node childRes = cache[current[i]];
+        result = nm->mkNode(current.getKind(), result, childRes);
       }
-      cache[current] = result;
-      toVisit.pop_back();
     }
     else
     {
-      // Mark that we have added the children if any
-      if (current.getNumChildren() > 0)
-      {
-        stackHead.d_children_added = true;
-        // We need to add the children
-        for (TNode::iterator child_it = current.begin();
-             child_it != current.end();
-             ++child_it)
-        {
-          TNode childNode = *child_it;
-          NodeMap::iterator childFind = cache.find(childNode);
-          if (childFind == cache.end())
-          {
-            toVisit.push_back(childNode);
-          }
-        }
+      NodeBuilder<> builder(current.getKind());
+      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        builder << current.getOperator();
       }
-      else
+
+      for (unsigned i = 0; i < current.getNumChildren(); ++i)
       {
-        cache[current] = current;
-        toVisit.pop_back();
+        Assert(cache.find(current[i]) != cache.end());
+        builder << cache[current[i]];
       }
+      result = builder;
     }
+    cache[current] = result;
   }
   return cache[n];
 }
@@ -147,30 +99,16 @@ Node intToBV(TNode n, NodeMap& cache)
   AlwaysAssert(size > 0);
   AlwaysAssert(!options::incrementalSolving());
 
-  vector<intToBV_stack_element> toVisit;
   NodeMap binaryCache;
   Node n_binary = intToBVMakeBinary(n, binaryCache);
-  toVisit.push_back(TNode(n_binary));
 
-  while (!toVisit.empty())
+  for (TNode current : NodeDfsIterable(n_binary, VisitOrder::POSTORDER,
+           [&cache](TNode nn) { return cache.count(nn) > 0; }))
   {
-    // The current node we are processing
-    intToBV_stack_element& stackHead = toVisit.back();
-    TNode current = stackHead.d_node;
-
-    // If node is already in the cache we're done, pop from the stack
-    NodeMap::iterator find = cache.find(current);
-    if (find != cache.end())
-    {
-      toVisit.pop_back();
-      continue;
-    }
-
-    // Not yet substituted, so process
     NodeManager* nm = NodeManager::currentNM();
-    if (stackHead.d_children_added)
+    if (current.getNumChildren() > 0)
     {
-      // Children have been processed, so rebuild this node
+      // Not a leaf
       vector<Node> children;
       unsigned max = 0;
       for (unsigned i = 0; i < current.getNumChildren(); ++i)
@@ -258,73 +196,51 @@ Node intToBV(TNode n, NodeMap& cache)
 
       result = Rewriter::rewrite(result);
       cache[current] = result;
-      toVisit.pop_back();
     }
     else
     {
-      // Mark that we have added the children if any
-      if (current.getNumChildren() > 0)
+      // It's a leaf: could be a variable or a numeral
+      Node result = current;
+      if (current.isVar())
       {
-        stackHead.d_children_added = true;
-        // We need to add the children
-        for (TNode::iterator child_it = current.begin();
-             child_it != current.end();
-             ++child_it)
+        if (current.getType() == nm->integerType())
         {
-          TNode childNode = *child_it;
-          NodeMap::iterator childFind = cache.find(childNode);
-          if (childFind == cache.end())
-          {
-            toVisit.push_back(childNode);
-          }
+          result = nm->mkSkolem("__intToBV_var",
+                                nm->mkBitVectorType(size),
+                                "Variable introduced in intToBV pass");
         }
       }
-      else
+      else if (current.isConst())
       {
-        // It's a leaf: could be a variable or a numeral
-        Node result = current;
-        if (current.isVar())
+        switch (current.getKind())
         {
-          if (current.getType() == nm->integerType())
+          case kind::CONST_RATIONAL:
           {
-            result = nm->mkSkolem("__intToBV_var",
-                                  nm->mkBitVectorType(size),
-                                  "Variable introduced in intToBV pass");
-          }
-        }
-        else if (current.isConst())
-        {
-          switch (current.getKind())
-          {
-            case kind::CONST_RATIONAL:
-            {
-              Rational constant = current.getConst<Rational>();
-              if (constant.isIntegral()) {
-                AlwaysAssert(constant >= 0);
-                BitVector bv(size, constant.getNumerator());
-                if (bv.toSignedInteger() != constant.getNumerator())
-                {
-                  throw TypeCheckingException(
-                      current.toExpr(),
-                      string("Not enough bits for constant in intToBV: ")
-                          + current.toString());
-                }
-                result = nm->mkConst(bv);
+            Rational constant = current.getConst<Rational>();
+            if (constant.isIntegral()) {
+              AlwaysAssert(constant >= 0);
+              BitVector bv(size, constant.getNumerator());
+              if (bv.toSignedInteger() != constant.getNumerator())
+              {
+                throw TypeCheckingException(
+                    current.toExpr(),
+                    string("Not enough bits for constant in intToBV: ")
+                        + current.toString());
               }
-              break;
+              result = nm->mkConst(bv);
             }
-            default: break;
+            break;
           }
+          default: break;
         }
-        else
-        {
-          throw TypeCheckingException(
-              current.toExpr(),
-              string("Cannot translate to BV: ") + current.toString());
-        }
-        cache[current] = result;
-        toVisit.pop_back();
       }
+      else
+      {
+        throw TypeCheckingException(
+            current.toExpr(),
+            string("Cannot translate to BV: ") + current.toString());
+      }
+      cache[current] = result;
     }
   }
   return cache[n_binary];
diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h
index 95f31621a..284cf7256 100644
--- a/src/preprocessing/passes/int_to_bv.h
+++ b/src/preprocessing/passes/int_to_bv.h
@@ -2,9 +2,9 @@
 /*! \file int_to_bv.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli
+ **   Andres Noetzli, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 6ad97f4a3..f021fff28 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -2,9 +2,9 @@
 /*! \file ite_removal.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli
+ **   Andres Noetzli, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h
index 5620b4afb..950d7342a 100644
--- a/src/preprocessing/passes/ite_removal.h
+++ b/src/preprocessing/passes/ite_removal.h
@@ -2,9 +2,9 @@
 /*! \file ite_removal.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli
+ **   Andres Noetzli, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 7f7c4c95f..9a6a8ec61 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Aina Niemetz, Tim King, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h
index 44976bded..cf122c4c9 100644
--- a/src/preprocessing/passes/ite_simp.h
+++ b/src/preprocessing/passes/ite_simp.h
@@ -2,9 +2,9 @@
 /*! \file ite_simp.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz
+ **   Aina Niemetz, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index debb4d2ac..f64fce118 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -2,9 +2,9 @@
 /*! \file miplib_trick.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner, Tim King, Andres Noetzli
+ **   Mathias Preiner, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h
index f1748d635..d57658d47 100644
--- a/src/preprocessing/passes/miplib_trick.h
+++ b/src/preprocessing/passes/miplib_trick.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index eb5728228..1f7e298ee 100644
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -2,9 +2,9 @@
 /*! \file nl_ext_purify.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h
index 7744df824..a3004a7e8 100644
--- a/src/preprocessing/passes/nl_ext_purify.h
+++ b/src/preprocessing/passes/nl_ext_purify.h
@@ -2,9 +2,9 @@
 /*! \file nl_ext_purify.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 03f38370b..6d2482a0e 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -2,9 +2,9 @@
 /*! \file non_clausal_simp.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Tim King, Andres Noetzli
+ **   Aina Niemetz, Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h
index cb4ece4a9..6e3645177 100644
--- a/src/preprocessing/passes/non_clausal_simp.h
+++ b/src/preprocessing/passes/non_clausal_simp.h
@@ -2,9 +2,9 @@
 /*! \file non_clausal_simp.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz
+ **   Aina Niemetz, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index d852f2d86..1f9ca579c 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h
index e73b721ff..fed566f78 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.h
+++ b/src/preprocessing/passes/pseudo_boolean_processor.h
@@ -2,9 +2,9 @@
 /*! \file pseudo_boolean_processor.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andres Noetzli
+ **   Tim King, Andres Noetzli, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index bc2c136e4..a4d8454a0 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -2,9 +2,9 @@
 /*! \file quantifier_macros.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Yoni Zohar, Morgan Deters
+ **   Andrew Reynolds, Yoni Zohar, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h
index 6b62c4d31..30a83e54a 100644
--- a/src/preprocessing/passes/quantifier_macros.h
+++ b/src/preprocessing/passes/quantifier_macros.h
@@ -2,9 +2,9 @@
 /*! \file quantifier_macros.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar, Andrew Reynolds
+ **   Yoni Zohar, Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp
index eb6017402..3052e9629 100644
--- a/src/preprocessing/passes/quantifiers_preprocess.cpp
+++ b/src/preprocessing/passes/quantifiers_preprocess.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Caleb Donovick
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h
index 991b3dd05..1e8b298f1 100644
--- a/src/preprocessing/passes/quantifiers_preprocess.h
+++ b/src/preprocessing/passes/quantifiers_preprocess.h
@@ -2,9 +2,9 @@
 /*! \file quantifiers_preprocess.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Caleb Donovick
+ **   Caleb Donovick, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index 1c77f6f54..0e8ee3c4d 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -2,9 +2,9 @@
 /*! \file real_to_int.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h
index 7949fb051..d5c3be4e5 100644
--- a/src/preprocessing/passes/real_to_int.h
+++ b/src/preprocessing/passes/real_to_int.h
@@ -2,9 +2,9 @@
 /*! \file real_to_int.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp
index deb58ae9f..e12691cc0 100644
--- a/src/preprocessing/passes/rewrite.cpp
+++ b/src/preprocessing/passes/rewrite.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Caleb Donovick
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h
index e83cafb85..3bced24b1 100644
--- a/src/preprocessing/passes/rewrite.h
+++ b/src/preprocessing/passes/rewrite.h
@@ -2,9 +2,9 @@
 /*! \file rewrite.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Caleb Donovick
+ **   Caleb Donovick, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index a81dbb4b5..b6f575789 100644
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Yoni Zohar, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h
index 1a5e36c40..8cbab3e29 100644
--- a/src/preprocessing/passes/sep_skolem_emp.h
+++ b/src/preprocessing/passes/sep_skolem_emp.h
@@ -2,9 +2,9 @@
 /*! \file sep_skolem_emp.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar
+ **   Yoni Zohar, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index d0612086c..92c2e55b1 100644
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h
index ae722529d..3a8646109 100644
--- a/src/preprocessing/passes/sort_infer.h
+++ b/src/preprocessing/passes/sort_infer.h
@@ -2,9 +2,9 @@
 /*! \file sort_infer.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Andres Noetzli
+ **   Andrew Reynolds, Mathias Preiner, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp
index ec3982e03..314c34617 100644
--- a/src/preprocessing/passes/static_learning.cpp
+++ b/src/preprocessing/passes/static_learning.cpp
@@ -2,9 +2,9 @@
 /*! \file static_learning.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar
+ **   Yoni Zohar, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h
index f200755c5..16498f080 100644
--- a/src/preprocessing/passes/static_learning.h
+++ b/src/preprocessing/passes/static_learning.h
@@ -2,9 +2,9 @@
 /*! \file static_learning.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar
+ **   Yoni Zohar, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 776e738d3..d8a587136 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -2,9 +2,9 @@
 /*! \file sygus_inference.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h
index 91deb445c..6b84ea3fe 100644
--- a/src/preprocessing/passes/sygus_inference.h
+++ b/src/preprocessing/passes/sygus_inference.h
@@ -2,9 +2,9 @@
 /*! \file sygus_inference.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index f1e9e39c5..699899c1e 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -2,9 +2,9 @@
 /*! \file synth_rew_rules.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h
index 38ef98b35..80e09fd11 100644
--- a/src/preprocessing/passes/synth_rew_rules.h
+++ b/src/preprocessing/passes/synth_rew_rules.h
@@ -2,9 +2,9 @@
 /*! \file synth_rew_rules.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 1399363fa..5cc25b73f 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h
index cfa9ab0b5..764685b85 100644
--- a/src/preprocessing/passes/theory_preprocess.h
+++ b/src/preprocessing/passes/theory_preprocess.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 5d544ae57..7d1f66d65 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -2,9 +2,9 @@
 /*! \file unconstrained_simplifier.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Clark Barrett, Andres Noetzli, Tim King
+ **   Clark Barrett, Andres Noetzli, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
@@ -75,6 +75,16 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
         {
           d_unconstrained.erase(current);
         }
+        else
+        {
+          // Also erase the children from the visited-once set when we visit a
+          // node a second time, otherwise variables in this node are not
+          // erased from the set of unconstrained variables.
+          for (TNode childNode : current)
+          {
+            toVisit.push_back(unc_preprocess_stack_element(childNode, current));
+          }
+        }
       }
       ++find->second;
       continue;
@@ -91,6 +101,15 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
         d_unconstrained.insert(current);
       }
     }
+    else if (current.isClosure())
+    {
+      // Throw an exception. This should never happen in practice unless the
+      // user specifically enabled unconstrained simplification in an illegal
+      // logic.
+      throw LogicException(
+          "Cannot use unconstrained simplification in this logic, due to "
+          "(possibly internally introduced) quantified formula.");
+    }
     else
     {
       for (TNode childNode : current)
diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h
index ac4fd0a03..c10730d60 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.h
+++ b/src/preprocessing/passes/unconstrained_simplifier.h
@@ -2,9 +2,9 @@
 /*! \file unconstrained_simplifier.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Clark Barrett, Andres Noetzli
+ **   Clark Barrett, Andres Noetzli, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
@@ -62,7 +62,11 @@ class UnconstrainedSimplifier : public PreprocessingPass
   theory::SubstitutionMap d_substitutions;
 
   const LogicInfo& d_logicInfo;
-
+  /**
+   * Visit all subterms in assertion. This method throws a LogicException if
+   * there is a subterm that is unhandled by this preprocessing pass (e.g. a
+   * quantified formula).
+   */
   void visitAll(TNode assertion);
   Node newUnconstrainedVar(TypeNode t, TNode var);
   void processUnconstrained();
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 84c3ca79b..965edcd2f 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Justin Xu, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index 4a2e71488..e81f71666 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -2,9 +2,9 @@
 /*! \file preprocessing_pass.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Justin Xu
+ **   Justin Xu, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 75085d7c4..c7e7ae82c 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Aina Niemetz, Mathias Preiner, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index f4317d786..deb600885 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -2,9 +2,9 @@
 /*! \file preprocessing_pass_context.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Mathias Preiner, Justin Xu
+ **   Aina Niemetz, Mathias Preiner, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index e264c17e5..59c03479e 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -2,9 +2,9 @@
 /*! \file preprocessing_pass_registry.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli, Justin Xu, Yoni Zohar
+ **   Andres Noetzli, Yoni Zohar, Justin Xu
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
index 9cc109897..cf10ab902 100644
--- a/src/preprocessing/preprocessing_pass_registry.h
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -2,9 +2,9 @@
 /*! \file preprocessing_pass_registry.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli, Justin Xu, Yoni Zohar
+ **   Andres Noetzli, Justin Xu, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index c609eebd7..45762341a 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Aina Niemetz, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index ad195e62e..d26dee206 100644
--- a/src/preprocessing/util/ite_utilities.h
+++ b/src/preprocessing/util/ite_utilities.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Aina Niemetz, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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