From cc659c968917351876cd9000e96469aefbdd8771 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <michael.tautschnig@qmul.ac.uk>
Date: Fri, 6 Jan 2017 23:57:30 +0000
Subject: [PATCH] Use a known constant offset when dereferencing

---
 src/pointer-analysis/value_set_dereference.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 1323ee31b5..0e4c966817 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -559,7 +559,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       result.value=o.root_object();
 
       // this is relative to the root object
-      const exprt offset=pointer_offset(pointer_expr);
+      exprt offset;
+      if(o.offset().id()==ID_unknown)
+        offset=pointer_offset(pointer_expr);
+      else
+        offset=o.offset();
 
       if(memory_model(result.value, dereference_type, tmp_guard, offset))
       {