Document bv-to-bool recursion (#3848)

The BV-to-bool pass is implemented recursively.
This commit documents that.
We may want to change it at some point.

diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index 0637c541f84bfd6908712e1d79b7918a2ac75639..de9504503d3940e60ca047f331d387ca52cdebb8 100644 (file)
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -12,6 +12,7 @@
  ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans.
  **
  ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
+ ** Implemented recursively.
  **/
 
 #include "preprocessing/passes/bv_to_bool.h"
@@ -258,6 +259,7 @@ Node BVToBool::liftNode(TNode current)
       }
       for (unsigned i = 0; i < current.getNumChildren(); ++i)
       {
+        // Recursively lift children
         Node converted = liftNode(current[i]);
         Assert(converted.getType() == current[i].getType());
         builder << converted;