Add Journault example of unsound heterogeneous join with integer poly…

…hedra

tests/regression/56-witness/48-apron-unassume-unsound-int-poly.c

@@ -0,0 +1,11 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 48-apron-unassume-unsound-int-poly.yml --enable ana.apron.strengthening --set sem.int.signed_overflow assume_none --set ana.apron.domain polyhedra
+#include <goblint.h>
+
+int main() {
+  int x, y;
+  if (x == 2 * y) {
+    __goblint_check(x == 2 * y); // UNKNOWN (intentional by unassume)
+    __goblint_check(x == 2 * y); // UNKNOWN (intentional by unassume)
+  }
+  return 0;
+}

tests/regression/56-witness/48-apron-unassume-unsound-int-poly.yml

@@ -0,0 +1,50 @@
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: dec4db01-03ed-47dd-ae55-c84f8dcd51ed
+    creation_time: 2022-09-13T11:38:16Z
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - 48-apron-unassume-unsound-int-poly.c
+      input_file_hashes:
+        48-apron-unassume-unsound-int-poly.c: b2a50e3b423ade600ec2de58fa8ace6ec9a08b85fdc016cbdb7fbe9a3ba80d83
+      data_model: LP64
+      language: C
+  location:
+    file_name: 48-apron-unassume-unsound-int-poly.c
+    file_hash: b2a50e3b423ade600ec2de58fa8ace6ec9a08b85fdc016cbdb7fbe9a3ba80d83
+    line: 7
+    column: 5
+    function: main
+  location_invariant:
+    string: x == 3
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: dec4db01-03ed-47dd-ae55-c84f8dcd51ee
+    creation_time: 2022-09-13T11:38:16Z
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - 48-apron-unassume-unsound-int-poly.c
+      input_file_hashes:
+        48-apron-unassume-unsound-int-poly.c: b2a50e3b423ade600ec2de58fa8ace6ec9a08b85fdc016cbdb7fbe9a3ba80d83
+      data_model: LP64
+      language: C
+  location:
+    file_name: 48-apron-unassume-unsound-int-poly.c
+    file_hash: b2a50e3b423ade600ec2de58fa8ace6ec9a08b85fdc016cbdb7fbe9a3ba80d83
+    line: 8
+    column: 5
+    function: main
+  location_invariant:
+    string: x == 3 && y >= 0
+    type: assertion
+    format: C