diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index 9456037a474..956c71949de 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -145,7 +145,7 @@ class interpretert:public messaget return 0; std::size_t ret=0; std::size_t alloc_size=base_address_to_alloc_size(address); - while(memory_iter!=memory.end() && retfirst<(address+alloc_size)) { ++ret; ++memory_iter;