// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.int.congruence --enable ana.int.congruence_no_overflow --enable ana.int.refinement
#include <assert.h>

int main(){
    int r = -103;
    for (int i = 0; i < 40; i++) {
        r = r + 5;
    }

    // At this point r in the congr. dom should be 2 + 5Z
    int k = r;
    if (k >= 3) {
        // After refinement with congruences, the lower bound should be 7 as the numbers 3 - 6 are not in the congr. class
        assert (k < 7); // FAIL
    }

    if (r >= -11 && r <= -4) {
        assert (r == -8);
    }
    return 0;
}

// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.int.congruence
#include <assert.h>

int main(){
    int r = -103;
    for (int i = 0; i < 40; i++) {
        r = r + 5;
    }
    // At this point r in the congr. dom should be 2 + 5Z
    int k = r;
    if (k >= 3) {
        // After refinement with congruences, the lower bound should be 7 as the numbers 3 - 6 are not in the congr. class
        assert (k < 7); // FAIL
    }

    if (r >= -11 && r <= -4) {
        assert (r == -8);
    }
    return 0;
}

--- 
+++ 
@@ -1,4 +1,4 @@
-// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.int.congruence
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.int.congruence --enable ana.int.congruence_no_overflow --enable ana.int.refinement
 #include <assert.h>
 
 int main(){
@@ -6,6 +6,7 @@
     for (int i = 0; i < 40; i++) {
         r = r + 5;
     }
+
     // At this point r in the congr. dom should be 2 + 5Z
     int k = r;
     if (k >= 3) {
Add updated params to interval-congruence ref. reg test
