Add test for general abs refinement

goblint · Nov 28, 2023 · cdf0dee · cdf0dee
1 parent 1730aa7
commit cdf0dee
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/tests/regression/39-signed-overflows/06-abs.c b/tests/regression/39-signed-overflows/06-abs.c
@@ -17,6 +17,13 @@ int main() {
             __goblint_check(-100 <= data);
             int result = data * data; //NOWARN
         }
+
+        if(abs(data) - 1 <= 99)
+        {
+            __goblint_check(data <= 100);
+            __goblint_check(-100 <= data);
+            int result = data * data; //NOWARN
+        }
     }
     return 8;
 }