From b778bea851d7d9f5d30ae860e0e0539b783a2205 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 13 Feb 2019 18:05:41 +0000 Subject: [PATCH] byte_update against a pointer shouldn't be fatal This can happen in inaccessible code, so it doesn't seem necessary to kill the whole process --- src/solvers/flattening/bv_pointers.cpp | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 9f47c211ab9..673621d4746 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -451,16 +451,6 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) { return SUB::convert_byte_extract(to_byte_extract_expr(expr)); } - else - { - INVARIANT( - expr.id() != ID_byte_update_little_endian, - "byte-wise pointer updates are unsupported"); - - INVARIANT( - expr.id() != ID_byte_update_big_endian, - "byte-wise pointer updates are unsupported"); - } return conversion_failed(expr); }