Do not unnecessary follow tag types when storing the boolbv mapping

Types in equations must match exactly, there is no need to follow tags
when checking for type consistency. Also, do not use a followed type
when storing the mapping. When retrieving a mapped value, assert type
consistency.

Author: tautschnig

src/solvers/flattening/boolbv.cpp

@@ -573,11 +573,11 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
   if(!equality_propagation)
     return true;
 
-  const typet &type=ns.follow(expr.lhs().type());
+  const typet &type = expr.lhs().type();
 
-  if(expr.lhs().id()==ID_symbol &&
-     type==ns.follow(expr.rhs().type()) &&
-     type.id()!=ID_bool)
+  if(
+    expr.lhs().id() == ID_symbol && type == expr.rhs().type() &&
+    type.id() != ID_bool)
   {
     // see if it is an unbounded array
     if(is_unbounded_array(type))

src/solvers/flattening/boolbv_get.cpp

@@ -31,6 +31,11 @@ exprt boolbvt::get(const exprt &expr) const
     if(it!=map.mapping.end())
     {
       const boolbv_mapt::map_entryt &map_entry=it->second;
+      // an input expression must either be untyped (this is used for obtaining
+      // the value of clock symbols, which do not have a fixed type as the clock
+      // type is computed during symbolic execution) or match the type stored in
+      // the mapping
+      PRECONDITION(expr.type() == typet() || expr.type() == map_entry.type);
 
       if(is_unbounded_array(map_entry.type))
         return bv_get_unbounded_array(expr);