bug fixed: simplify usage

benchmark/case_0.c

@@ -3,7 +3,8 @@
 int main(){
     // int whatever;
     int * data = malloc(2*sizeof(int));
-    int i = *data;
+    int * data2 = malloc(sizeof(int));  
+    int i = *(data + 1);
     free(data);
     // int* j = NULL;
     // int* i = j;

src/goto-symex/builtin_functions.cpp

@@ -243,6 +243,7 @@ expr2tc goto_symext::symex_mem(
     return to_address_of2t(rhs_addrof).ptr_obj;
 
   } else {
+    log_status("create heap symbol for allocation");
     unsigned int &dynamic_counter = get_dynamic_counter();
     dynamic_counter++;
 
@@ -259,12 +260,18 @@ expr2tc goto_symext::symex_mem(
 
     symbol.type.dynamic(true);
     symbol.mode = "C";
+    log_status("new_context.add(symbol);");
     new_context.add(symbol);
 
     type2tc heap_type = get_intheap_type();
     expr2tc allocated_heap = symbol2tc(heap_type, symbol.id);
     std::vector<expr2tc> pts;
-    expr2tc size_simplified = size.simplify();
+    expr2tc size_simplified;
+    if(!is_constant_int2t(size)) {
+      size_simplified = size.simplify();
+    } else {
+      size_simplified = size;
+    }
     guardt alloc_guard = cur_state->guard;
     // TODO SLHV: add size simplification later
     if(!is_constant_int2t(size_simplified)) {

src/goto-symex/symex_assign.cpp

@@ -192,9 +192,7 @@ void goto_symext::symex_assign(
   dereference(lhs, dereferencet::WRITE);
   log_status("dereference rhs read");
   dereference(rhs, dereferencet::READ);
-  log_status("replace dynamic allocation lhs");
   replace_dynamic_allocation(lhs);
-  log_status("replace dynamic allocation rhs");
   replace_dynamic_allocation(rhs);
 
   // printf expression that has lhs

src/goto-symex/symex_valid_object.cpp

@@ -25,7 +25,6 @@ void goto_symext::replace_dynamic_allocation(expr2tc &expr)
   if (is_nil_expr(expr))
     return;
 
-  log_status("replace dynamic allocation");
   expr->Foreach_operand([this](expr2tc &e) { replace_dynamic_allocation(e); });
 
   if (is_valid_object2t(expr) || is_deallocated_obj2t(expr))