diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp index c57a6469c29..c6a5ded5613 100644 --- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp +++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp @@ -1459,7 +1459,7 @@ exprt c_typecheck_baset::typecheck_shuffle_vector( operands.push_back(std::move(mod_index)); } - return shuffle_vector_exprt{arg0, arg1, std::move(operands)}.lower(); + return shuffle_vector_exprt{arg0, arg1, std::move(operands)}; } else if(identifier == "__builtin_shufflevector") { @@ -1509,8 +1509,8 @@ exprt c_typecheck_baset::typecheck_shuffle_vector( } } - return shuffle_vector_exprt{arguments[0], arguments[1], std::move(operands)} - .lower(); + return shuffle_vector_exprt{ + arguments[0], arguments[1], std::move(operands)}; } else UNREACHABLE; diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 217d351f443..7b0bcfd6c03 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -16,6 +16,8 @@ Date: September 2014 #include #include +#include + #include "goto_model.h" static bool have_to_remove_vector(const typet &type); @@ -41,6 +43,8 @@ static bool have_to_remove_vector(const exprt &expr) { return true; } + else if(expr.id() == ID_shuffle_vector) + return true; else if(expr.id()==ID_vector) return true; } @@ -93,6 +97,14 @@ static void remove_vector(exprt &expr) if(!have_to_remove_vector(expr)) return; + if(expr.id() == ID_shuffle_vector) + { + exprt result = to_shuffle_vector_expr(expr).lower(); + remove_vector(result); + expr.swap(result); + return; + } + Forall_operands(it, expr) remove_vector(*it);