Merge branch 'master' into lfscTestslfscTests

1 files changed, 7 insertions, 3 deletions

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();