break statement does not break from loop

[eleehiga]

For the following code:

#include <errno.h>
#include <limits.h>
#include <stdarg.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <time.h>

void strtod(char *str, char **ptr) {
  *ptr = str;
}

void test(char *s) {
        int i = 0;
        char *parse_end, *string_end;
        string_end = s + strlen(s);
        while(s < string_end) {
        strtod(s, &parse_end);
        if(parse_end == s) {
                i = -1;
                break;
        }
        }
        assert(i == -1);
}

void test_harness() {
        test("t");
}

Running the command cbmc test.c --function test_harness will infinitely repeat a line like Unwinding loop test.0 iteration 580 file test.c line 16 function test thread 0. I thought that this would go to the break statement but it appears that it does not. As when I comment out the while and break statement in the code above the assertion will hold that the variable i has changed from 0 to -1 and therefore that means that parse_end == s will be true for this code. Therefore, can you guys please help me understand why the break statement is not breaking the loop?

[tautschnig]

It seems algebraic simplification did not consider the case of string constants when doing pointer comparison. Fixed in #6967. (Running this example with --unwind 2 --unwinding-assertions always produced the correct result.)

[eleehiga]

@tautschnig and @kroening Thank you guys for making this change.