Update cram test

goblint · Dec 17, 2024 · cf2641f · cf2641f
1 parent d54dfcc
commit cf2641f
Show file tree

Hide file tree

Showing 2 changed files with 248 additions and 72 deletions.
diff --git a/tests/regression/46-apron2/95-witness-mm-escape.t b/tests/regression/46-apron2/95-witness-mm-escape.t
@@ -7,19 +7,23 @@
   [Success][Witness] invariant confirmed: 0 <= *b (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: g <= 127 (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: *b <= 127 (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: -8LL + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 2147483648LL + (long long )a >= 0LL (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: (2147483638LL + (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: (2147483637LL - (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 10LL - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 2147483647LL - (long long )a >= 0LL (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: (2147483658LL + (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: (2147483657LL - (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: b == & g (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: g != 0 (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: *b != 0 (95-witness-mm-escape.c:19:1)
   [Info][Witness] witness validation summary:
-    confirmed: 22
+    confirmed: 30
     unconfirmed: 0
     refuted: 0
     error: 0
     unchecked: 0
     unsupported: 0
     disabled: 0
-    total validation entries: 22
+    total validation entries: 30