fixup! Value set: lift offset from numeric constants to expressions

Kani's test `tests/kani/Iterator/flat_map.rs` does reach this branch.

Author: tautschnig

src/pointer-analysis/value_set.cpp

@@ -28,9 +28,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol.h>
 #include <util/xml.h>
 
-#ifdef DEBUG
+//#ifdef DEBUG
 #  include <iostream>
-#endif
+//#endif
 
 #include "add_failed_symbols.h"
 
@@ -356,21 +356,6 @@ bool value_sett::eval_pointer_offset(
         return false;
       else
       {
-        // This branch should not be reached as any constant offset will have
-        // been used before already. The following code will trigger
-        // `eval_pointer_offset`, yet we wouldn't end up in this branch:
-        // struct S { int a; char b; };
-        //
-        // int main()
-        // {
-        //   struct S s;
-        //   int offset;
-        //   __CPROVER_assume(offset >= 0 && offset <= 1 && offset % 2 == 0);
-        //   int *p = (char*)&s + offset;
-        //   int x = *p;
-        //   __CPROVER_assert(s.a == x, "");
-        // }
-        UNREACHABLE;
         const exprt &object=object_numbering[it->first];
         auto ptr_offset = compute_pointer_offset(object, ns);
 
@@ -1151,6 +1136,7 @@ void value_sett::get_value_set_rec(
       byte_extract_expr.op().type().id() == ID_struct_tag)
     {
       exprt offset = byte_extract_expr.offset();
+      std::cerr << "EXPR: " << format(expr) << std::endl;
       if(eval_pointer_offset(offset, ns))
         simplify(offset, ns);