Merge pull request #4364 from tautschnig/mapping-dont-follow

Do not unnecessary follow tag types when storing the boolbv mapping

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