// PARAM: --enable ana.int.congruence
void unsignedCase() {
    unsigned int top;
    unsigned int i = 0;
    if(top % 17 == 3) {
        assert(top%17 ==3);
        if(top %17 != 3) {
            i = 12;
        } else {

        }
    }
    assert(i ==0);

    if(top % 17 == 0) {
        assert(top%17 == 0);
        if(top %17 != 0) {
            i = 12;
        }
    }
    assert(i == 0);

    if(top % 3 == 17) {
        // This is unreachable in the concrete!
        assert(top%17 == 3); //UNKNOWN!
    }
}

int main() {
    int top;
    int i = 0;
    if(top % 17 == 3) {
        assert(top%17 ==3);
        if(top %17 != 3) {
            i = 12;
        } else {

        }
    }
    assert(i ==0);

    if(top % 17 == 0) {
        assert(top%17 == 0);
        if(top %17 != 0) {
            i = 12;
        }
    }
    assert(i == 0);

    if(top % 3 == 17) {
        // This is unreachable in the concrete!
        assert(top%17 == 3); //UNKNOWN!
    }

    unsignedCase();
}

// PARAM: --enable ana.int.congruence
void unsignedCase() {
    unsigned int top;
    unsigned int i = 0;
    if(top % 17 == 3) {
        assert(top%17 ==3);
        if(top %17 != 3) {
            i = 12;
        } else {

        }
    }
    assert(i ==0);

    if(top % 17 == 0) {
        assert(top%17 == 0);
        if(top %17 != 0) {
            i = 12;
        }
    }
    assert(i == 0);

    if(top % 3 == 17) {
        assert(top%17 == 3); //UNKNOWN!
    }
}

int main() {
    int top;
    int i = 0;
    if(top % 17 == 3) {
        assert(top%17 ==3);
        if(top %17 != 3) {
            i = 12;
        } else {

        }
    }
    assert(i ==0);

    if(top % 17 == 0) {
        assert(top%17 == 0);
        if(top %17 != 0) {
            i = 12;
        }
    }
    assert(i == 0);

    if(top % 3 == 17) {
        assert(top%17 == 3); //UNKNOWN!
    }

    unsignedCase();
}

--- 
+++ 
@@ -21,6 +21,7 @@
     assert(i == 0);
 
     if(top % 3 == 17) {
+        // This is unreachable in the concrete!
         assert(top%17 == 3); //UNKNOWN!
     }
 }
@@ -47,6 +48,7 @@
     assert(i == 0);
 
     if(top % 3 == 17) {
+        // This is unreachable in the concrete!
         assert(top%17 == 3); //UNKNOWN!
     }
 
Add comments to confusing test
