printf prints the wrong number for floats

[pablo-mendoza]

This program:

#include <stdio.h>
int main(void)
{
        printf ("%.0f %d\n", 1.0, 1);
}

will print "1 1" when run on its own, but when run under retrace v2 would print "0 1"

[ronaldtse]

@riataman good find -- can we add a test for this?

[pablo-mendoza]

I need to revamp the tests, I don't think we are running any tests for v2 right now.