From c93dd787d6ff4a6098b2db0a8dba008874c15ef8 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com>
Date: Thu, 16 Nov 2017 14:34:02 +0000
Subject: [PATCH] Remove too tight precondition in evaluator that was causing
 an invariant violation in some cases.

---
 src/goto-programs/interpreter_evaluate.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 0a2a7ec6e72..10b352090c3 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -1196,8 +1196,6 @@ mp_integer interpretert::evaluate_address(
     if(expr.operands().size()!=1)
       throw "typecast expects one operand";
 
-    PRECONDITION(expr.type().id()==ID_pointer);
-
     return evaluate_address(expr.op0(), fail_quietly);
   }
   if(!fail_quietly)