Add test 56-witness/48-apron-unassume-no-strengthening

Author: sim642

tests/regression/56-witness/48-apron-unassume-no-strengthening.c

@@ -0,0 +1,14 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain interval --set ana.activated[+] unassume --set witness.yaml.unassume 48-apron-unassume-no-strengthening.yml --disable ana.apron.strengthening
+#include <goblint.h>
+
+int main() {
+  int i = 0;
+  int j;
+  if (j < 100) {
+    __goblint_check(i == 0); // UNKNOWN (intentional by unassume)
+    __goblint_check(i >= 0);
+    __goblint_check(i < 100);
+    __goblint_check(j < 100);
+  }
+  return 0;
+}

tests/regression/56-witness/48-apron-unassume-no-strengthening.yml

@@ -0,0 +1,34 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "2.0"
+    uuid: 9b19e72a-376d-4c34-80d4-f46020de0c92
+    creation_time: 2025-03-12T12:53:06Z
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - 48-apron-unassume-no-strengthening.c
+      input_file_hashes:
+        48-apron-unassume-no-strengthening.c: 57377f1e739e562d852b16206d5b1092e2188d3a4fe89bfca405a81bde0e1546
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 48-apron-unassume-no-strengthening.c
+        line: 8
+        column: 5
+        function: main
+      value: i >= 0
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 48-apron-unassume-no-strengthening.c
+        line: 8
+        column: 5
+        function: main
+      value: i < 100
+      format: c_expression

tests/regression/56-witness/dune

@@ -22,6 +22,7 @@
      (run %{update_suite} bh-ex1-poly -q)
      (run %{update_suite} apron-unassume-precheck -q)
      (run %{update_suite} apron-tracked-global-annot -q)
+     (run %{update_suite} apron-unassume-no-strengthening -q)
      (run %{update_suite} apron-unassume-set-tokens -q)))))
 
 (cram