Allow function call results to be interrogated with history variables

[JustusAdam]

Results of function calls are not allowed to be interrogated in the history. For instance when compiling this example with goto-cc

int deref(int * i) {
    return *i;
}


void modify(int * ptr) 
__CPROVER_ensures(__CPROVER_old(deref(ptr)) + 4 == *ptr)
{
    *ptr += 4;
}


int main() {
    int i = 0;
    modify(&i);
    return 0;
}

We get the error

old_test_2.c: In function 'modify':
old_test_2.c:7:1: error: Tracking history of side_effect expressions is not supported yet.
 __CPROVER_ensures(__CPROVER_old(deref(ptr)) + 4 == *ptr)
CONVERSION ERROR

However the implementation of history variables is simply a storing into a temporary variable, which should be possible even through function calls.