From d73135a253df5f90f751050680ec3ee0933378f1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 23 May 2021 22:37:42 +0000 Subject: [PATCH] bv_pointerst: else case is just for byte updates We should not treat all other expressions as byte updates. Expressions other than those handled in the if/else if chain should result in failing conversion. --- src/solvers/flattening/bv_pointers.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index b73c7129d33..0290ccae0f7 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -508,7 +508,9 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) { return SUB::convert_byte_extract(to_byte_extract_expr(expr)); } - else + else if( + expr.id() == ID_byte_update_little_endian || + expr.id() == ID_byte_update_big_endian) { return SUB::convert_byte_update(to_byte_update_expr(expr)); }