functionst is a lowering, not a flattening

No bit-flattening is happening in this reduction.

Author: Daniel Kroening

src/solvers/Makefile

@@ -135,12 +135,12 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/bv_utils.cpp \
       flattening/c_bit_field_replacement_type.cpp \
       flattening/equality.cpp \
-      flattening/functions.cpp \
       flattening/pointer_logic.cpp \
       floatbv/float_bv.cpp \
       floatbv/float_utils.cpp \
       floatbv/float_approximation.cpp \
       lowering/byte_operators.cpp \
+      lowering/functions.cpp \
       lowering/popcount.cpp \
       bdd/miniBDD/miniBDD.cpp \
       prop/bdd_expr.cpp \

src/solvers/flattening/boolbv.h

@@ -19,11 +19,12 @@ Author: Daniel Kroening, [email protected]
 #include <util/mp_arith.h>
 #include <util/optional.h>
 
+#include <solvers/lowering/functions.h>
+
 #include "bv_utils.h"
 #include "boolbv_width.h"
 #include "boolbv_map.h"
 #include "arrays.h"
-#include "functions.h"
 
 class extractbit_exprt;
 class extractbits_exprt;