diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.t b/tests/regression/46-apron2/96-witness-mm-escape2.t index a109e44b48..07825f2af5 100644 --- a/tests/regression/46-apron2/96-witness-mm-escape2.t +++ b/tests/regression/46-apron2/96-witness-mm-escape2.t @@ -6,10 +6,6 @@ total generation entries: 6 $ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c - [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5) - [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1) - [Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1) - [Success][Witness] invariant confirmed: g != 0 (96-witness-mm-escape2.c:22:1) [Warning][Witness] cannot validate entry of type flow_insensitive_invariant [Info][Witness] witness validation summary: confirmed: 8 @@ -20,3 +16,7 @@ unsupported: 1 disabled: 0 total validation entries: 9 + [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5) + [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1) + [Success][Witness] invariant confirmed: g != 0 (96-witness-mm-escape2.c:22:1) + [Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1)