Remark on issue with fractional coefficients

goblint · Jan 12, 2024 · ca18e35 · ca18e35
1 parent f99f320
commit ca18e35
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/tests/regression/63-affeq/19-witness.c b/tests/regression/63-affeq/19-witness.c
@@ -15,4 +15,20 @@ void main(void) {
         j = j + 3;
     }
     __goblint_check(3 * i - j + k == 1);
+
+    // Represented with fractional coefficients and thus not put into witness yet
+
+    int a = 0;
+    int b = 0;
+    int z = 0;
+
+    while(z < 100) {
+        a++;
+        b += 2;
+        z++;
+
+        __goblint_check(2*z - b == 0);
+        // b == 2*z is put into the witness
+    }
+
 }