Specify witness.yaml.entry-types location/loop_invariant in witness tests with old YAML witnesses

sim642 · sim642 · commit a17e50d53b2a · 2025-04-17T19:49:37.000+03:00
diff --git a/tests/regression/56-witness/01-base-lor-enums.c b/tests/regression/56-witness/01-base-lor-enums.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.enums --set witness.yaml.validate 01-base-lor-enums.yml
+// PARAM: --enable ana.int.enums --set witness.yaml.entry-types[*] location_invariant --set witness.yaml.validate 01-base-lor-enums.yml
 
 int main() {
   int r; // rand
diff --git a/tests/regression/56-witness/02-base-lor-addr.c b/tests/regression/56-witness/02-base-lor-addr.c
@@ -1,4 +1,4 @@
-// PARAM: --set witness.yaml.validate 02-base-lor-addr.yml
+// PARAM: --set witness.yaml.entry-types[*] location_invariant --set witness.yaml.validate 02-base-lor-addr.yml
 
 int main() {
   int r; // rand
diff --git a/tests/regression/56-witness/03-int-log-short.c b/tests/regression/56-witness/03-int-log-short.c
@@ -1,4 +1,4 @@
-// PARAM: --set witness.yaml.validate 03-int-log-short.yml
+// PARAM: --set witness.yaml.entry-types[*] location_invariant --set witness.yaml.validate 03-int-log-short.yml
 
 int main() {
   int r;
diff --git a/tests/regression/56-witness/04-base-priv-sync-prune.c b/tests/regression/56-witness/04-base-priv-sync-prune.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.base.privatization write+lock --enable ana.int.interval --set witness.yaml.validate 04-base-priv-sync-prune.yml
+// SKIP PARAM: --set ana.base.privatization write+lock --enable ana.int.interval --set witness.yaml.entry-types[*] location_invariant --set witness.yaml.validate 04-base-priv-sync-prune.yml
 // TODO: fix unsoundness in base priv syncs
 #include <pthread.h>
 
diff --git a/tests/regression/56-witness/07-base-lor-interval.c b/tests/regression/56-witness/07-base-lor-interval.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set witness.yaml.validate 07-base-lor-interval.yml
+// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] location_invariant --set witness.yaml.validate 07-base-lor-interval.yml
 #include <goblint.h>
 
 int main() {
diff --git a/tests/regression/56-witness/10-apron-unassume-interval.c b/tests/regression/56-witness/10-apron-unassume-interval.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.activated[+] unassume --set witness.yaml.unassume 10-apron-unassume-interval.yml
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 10-apron-unassume-interval.yml
 #include <assert.h>
 // Using polyhedra instead of octagon, because the former has no narrowing and really needs the witness.
 int main() {
diff --git a/tests/regression/56-witness/11-base-unassume-interval.c b/tests/regression/56-witness/11-base-unassume-interval.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 11-base-unassume-interval.yml
+// SKIP PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 11-base-unassume-interval.yml
 #include <assert.h>
 
 int main() {
diff --git a/tests/regression/56-witness/12-apron-unassume-branch.c b/tests/regression/56-witness/12-apron-unassume-branch.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 12-apron-unassume-branch.yml --set ana.apron.domain polyhedra --enable ana.widen.tokens
+// SKIP PARAM: --set ana.activated[+] apron --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 12-apron-unassume-branch.yml --set ana.apron.domain polyhedra --enable ana.widen.tokens
 #include <assert.h>
 // Uses polyhedra instead of octagon such that widening tokens are actually needed by test instead of narrowing.
 int main() {
diff --git a/tests/regression/56-witness/13-base-unassume-branch.c b/tests/regression/56-witness/13-base-unassume-branch.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 13-base-unassume-branch.yml
+// SKIP PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 13-base-unassume-branch.yml
 #include <assert.h>
 
 int main() {
diff --git a/tests/regression/56-witness/14-base-unassume-precondition.c b/tests/regression/56-witness/14-base-unassume-precondition.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 14-base-unassume-precondition.yml --set witness.yaml.entry-types[+] precondition_loop_invariant
+// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 14-base-unassume-precondition.yml --set witness.yaml.entry-types[+] loop_invariant --set witness.yaml.entry-types[+] precondition_loop_invariant
 #include <assert.h>
 
 void foo(int n) {
diff --git a/tests/regression/56-witness/15-base-unassume-query.c b/tests/regression/56-witness/15-base-unassume-query.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] unassume --set witness.yaml.unassume 15-base-unassume-query.yml
+// PARAM: --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 15-base-unassume-query.yml
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/56-witness/16-base-unassume-dependent.c b/tests/regression/56-witness/16-base-unassume-dependent.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] unassume --set witness.yaml.unassume 16-base-unassume-dependent.yml --enable ana.int.interval
+// PARAM: --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 16-base-unassume-dependent.yml --enable ana.int.interval
 #include <goblint.h>
 
 int main() {
diff --git a/tests/regression/56-witness/17-base-unassume-tauto.c b/tests/regression/56-witness/17-base-unassume-tauto.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] unassume --set witness.yaml.unassume 17-base-unassume-tauto.yml --enable ana.int.interval --set ana.base.invariant.unassume fixpoint
+// PARAM: --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 17-base-unassume-tauto.yml --enable ana.int.interval --set ana.base.invariant.unassume fixpoint
 #include <goblint.h>
 
 int main() {
diff --git a/tests/regression/56-witness/18-base-unassume-contra.c b/tests/regression/56-witness/18-base-unassume-contra.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] unassume --set witness.yaml.unassume 18-base-unassume-contra.yml --enable ana.int.interval
+// PARAM: --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 18-base-unassume-contra.yml --enable ana.int.interval
 #include <goblint.h>
 
 int main() {
diff --git a/tests/regression/56-witness/19-base-unassume-mem.c b/tests/regression/56-witness/19-base-unassume-mem.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] unassume --set witness.yaml.unassume 19-base-unassume-mem.yml --enable ana.int.interval
+// PARAM: --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 19-base-unassume-mem.yml --enable ana.int.interval
 #include <goblint.h>
 
 int main() {
diff --git a/tests/regression/56-witness/20-apron-unassume-global.c b/tests/regression/56-witness/20-apron-unassume-global.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 20-apron-unassume-global.yml
+// SKIP PARAM: --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 20-apron-unassume-global.yml
 #include <assert.h>
 
 int i = 0;
diff --git a/tests/regression/56-witness/21-apron-unassume-priv.c b/tests/regression/56-witness/21-apron-unassume-priv.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.base.privatization none --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 21-apron-unassume-priv.yml
+// SKIP PARAM: --set ana.base.privatization none --set ana.activated[+] apron --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 21-apron-unassume-priv.yml
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/56-witness/22-base-unassume-priv.c b/tests/regression/56-witness/22-base-unassume-priv.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 22-base-unassume-priv.yml
+// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 22-base-unassume-priv.yml
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/56-witness/23-base-unassume-priv2.c b/tests/regression/56-witness/23-base-unassume-priv2.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 23-base-unassume-priv2.yml --set solvers.td3.side_widen always --enable ana.widen.tokens
+// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 23-base-unassume-priv2.yml --set solvers.td3.side_widen always --enable ana.widen.tokens
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/56-witness/24-apron-unassume-priv2.c b/tests/regression/56-witness/24-apron-unassume-priv2.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.base.privatization none --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 24-apron-unassume-priv2.yml  --set solvers.td3.side_widen always --enable ana.widen.tokens
+// SKIP PARAM: --set ana.base.privatization none --set ana.activated[+] apron --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 24-apron-unassume-priv2.yml  --set solvers.td3.side_widen always --enable ana.widen.tokens
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/56-witness/25-apron-unassume-strengthening.c b/tests/regression/56-witness/25-apron-unassume-strengthening.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 25-apron-unassume-strengthening.yml --enable ana.apron.strengthening --set sem.int.signed_overflow assume_none --set ana.apron.domain octagon
+// SKIP PARAM: --set ana.activated[+] apron --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 25-apron-unassume-strengthening.yml --enable ana.apron.strengthening --set sem.int.signed_overflow assume_none --set ana.apron.domain octagon
 #include <goblint.h>
 
 int main() {
diff --git a/tests/regression/56-witness/26-mine-tutorial-ex4.6.c b/tests/regression/56-witness/26-mine-tutorial-ex4.6.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 26-mine-tutorial-ex4.6.yml
+// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 26-mine-tutorial-ex4.6.yml
 #include <goblint.h>
 int main() {
   int x = 40;
diff --git a/tests/regression/56-witness/27-mine-tutorial-ex4.7.c b/tests/regression/56-witness/27-mine-tutorial-ex4.7.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set ana.activated[+] unassume --set witness.yaml.unassume 27-mine-tutorial-ex4.7.yml
+// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 27-mine-tutorial-ex4.7.yml
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
diff --git a/tests/regression/56-witness/28-mine-tutorial-ex4.8.c b/tests/regression/56-witness/28-mine-tutorial-ex4.8.c
@@ -1,4 +1,4 @@
-// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.activated[+] unassume --set witness.yaml.unassume 28-mine-tutorial-ex4.8.yml
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 28-mine-tutorial-ex4.8.yml
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
diff --git a/tests/regression/56-witness/29-mine-tutorial-ex4.10.c b/tests/regression/56-witness/29-mine-tutorial-ex4.10.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.activated[+] unassume --set witness.yaml.unassume 29-mine-tutorial-ex4.10.yml
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 29-mine-tutorial-ex4.10.yml
 // Using Apron polyhedra to have no narrowing.
 #include <goblint.h>
 int main() {
diff --git a/tests/regression/56-witness/30-base-unassume-inc-dec.c b/tests/regression/56-witness/30-base-unassume-inc-dec.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 30-base-unassume-inc-dec.yml --set solvers.td3.side_widen always --enable ana.widen.tokens
+// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 30-base-unassume-inc-dec.yml --set solvers.td3.side_widen always --enable ana.widen.tokens
 #include <pthread.h>
 #include <goblint.h>
 int g = 0;
diff --git a/tests/regression/56-witness/31-base-unassume-mem-ex.c b/tests/regression/56-witness/31-base-unassume-mem-ex.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 31-base-unassume-mem-ex.yml
+// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 31-base-unassume-mem-ex.yml
 #include <goblint.h>
 int main() {
   int i, j;
diff --git a/tests/regression/56-witness/32-base-unassume-lor-addr.c b/tests/regression/56-witness/32-base-unassume-lor-addr.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 32-base-unassume-lor-addr.yml
+// SKIP PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 32-base-unassume-lor-addr.yml
 // TODO: AD refine in invariant
 #include <goblint.h>
 int main() {
diff --git a/tests/regression/56-witness/33-base-unassume-lor-enums.c b/tests/regression/56-witness/33-base-unassume-lor-enums.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.enums --set ana.activated[+] unassume --set witness.yaml.unassume 33-base-unassume-lor-enums.yml
+// PARAM: --enable ana.int.enums --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 33-base-unassume-lor-enums.yml
 #include <goblint.h>
 int main() {
   int i;
diff --git a/tests/regression/56-witness/34-base-unassume-inc-dec-traces.c b/tests/regression/56-witness/34-base-unassume-inc-dec-traces.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 34-base-unassume-inc-dec-traces.yml --set solvers.td3.side_widen always --enable ana.widen.tokens --set ana.base.privatization write+lock
+// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 34-base-unassume-inc-dec-traces.yml --set solvers.td3.side_widen always --enable ana.widen.tokens --set ana.base.privatization write+lock
 #include <pthread.h>
 #include <goblint.h>
 int g = 0;
diff --git a/tests/regression/56-witness/35-hh-ex1b.c b/tests/regression/56-witness/35-hh-ex1b.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --disable solvers.td3.remove-wpoint --set ana.activated[+] unassume --set witness.yaml.unassume 35-hh-ex1b.yml
+// PARAM: --enable ana.int.interval --disable solvers.td3.remove-wpoint --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 35-hh-ex1b.yml
 #include <goblint.h>
 int main() {
   int i = 0;
diff --git a/tests/regression/56-witness/36-hh-ex2b.c b/tests/regression/56-witness/36-hh-ex2b.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set ana.activated[+] unassume --set witness.yaml.unassume 36-hh-ex2b.yml
+// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 36-hh-ex2b.yml
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
diff --git a/tests/regression/56-witness/37-hh-ex3.c b/tests/regression/56-witness/37-hh-ex3.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable ana.apron.strengthening --disable solvers.td3.remove-wpoint --set ana.activated[+] unassume --set witness.yaml.unassume 37-hh-ex3.yml
+// SKIP PARAM: --set ana.activated[+] apron --enable ana.apron.strengthening --disable solvers.td3.remove-wpoint --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 37-hh-ex3.yml
 #include <goblint.h>
 int main() {
   int i = 0;
diff --git a/tests/regression/56-witness/38-bh-ex3.c b/tests/regression/56-witness/38-bh-ex3.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set ana.activated[+] unassume --set witness.yaml.unassume 38-bh-ex3.yml
+// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 38-bh-ex3.yml
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
diff --git a/tests/regression/56-witness/39-bh-ex-add.c b/tests/regression/56-witness/39-bh-ex-add.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set ana.activated[+] unassume --set witness.yaml.unassume 39-bh-ex-add.yml
+// PARAM: --enable ana.int.interval --enable ana.sv-comp.functions --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 39-bh-ex-add.yml
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
diff --git a/tests/regression/56-witness/40-bh-ex1-poly.c b/tests/regression/56-witness/40-bh-ex1-poly.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.activated[+] unassume --set witness.yaml.unassume 40-bh-ex1-poly.yml --set sem.int.signed_overflow assume_none
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 40-bh-ex1-poly.yml --set sem.int.signed_overflow assume_none
 // TODO: why need to assume no overflow?
 #include <goblint.h>
 int main() {
diff --git a/tests/regression/56-witness/41-as-hybrid.c b/tests/regression/56-witness/41-as-hybrid.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 41-as-hybrid.yml
+// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 41-as-hybrid.yml
 #include <goblint.h>
 int main() {
   int i = 0;
diff --git a/tests/regression/56-witness/42-base-unassume-precheck.c b/tests/regression/56-witness/42-base-unassume-precheck.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] unassume --set witness.yaml.unassume 42-base-unassume-precheck.yml --enable ana.int.interval
+// PARAM: --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 42-base-unassume-precheck.yml --enable ana.int.interval
 #include <goblint.h>
 // ana.unassume.precheck not required? propagation unassume automatically skips?
 int main() {
diff --git a/tests/regression/56-witness/43-apron-unassume-precheck.c b/tests/regression/56-witness/43-apron-unassume-precheck.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 43-apron-unassume-precheck.yml --enable ana.unassume.precheck
+// SKIP PARAM: --set ana.activated[+] apron --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 43-apron-unassume-precheck.yml --enable ana.unassume.precheck
 #include <goblint.h>
 
 int main() {
diff --git a/tests/regression/56-witness/44-base-unassume-array.c b/tests/regression/56-witness/44-base-unassume-array.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] unassume --set witness.yaml.unassume 44-base-unassume-array.yml --enable ana.int.interval
+// PARAM: --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 44-base-unassume-array.yml --enable ana.int.interval
 #include <goblint.h>
 
 int main() {
diff --git a/tests/regression/56-witness/45-apron-tracked-global-annot.c b/tests/regression/56-witness/45-apron-tracked-global-annot.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --enable annotation.goblint_relation_track --set ana.activated[+] unassume --set witness.yaml.unassume 45-apron-tracked-global-annot.yml
+// SKIP PARAM: --set ana.activated[+] apron --enable annotation.goblint_relation_track --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 45-apron-tracked-global-annot.yml
 #include <goblint.h>
 
 int g __attribute__((__goblint_relation_track__)) = 0;
diff --git a/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.c b/tests/regression/56-witness/62-tm-inv-transfer-protection-witness.c
@@ -1,4 +1,4 @@
-// PARAM: --set solvers.td3.side_widen always --enable ana.int.interval --set ana.base.privatization protection --set "ana.activated[+]" unassume --set witness.yaml.unassume 62-tm-inv-transfer-protection-witness.yml --enable ana.widen.tokens
+// PARAM: --set solvers.td3.side_widen always --enable ana.int.interval --set ana.base.privatization protection --set witness.yaml.entry-types[*] location_invariant --set "ana.activated[+]" unassume --set witness.yaml.unassume 62-tm-inv-transfer-protection-witness.yml --enable ana.widen.tokens
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/56-witness/63-hh-ex3-term.c b/tests/regression/56-witness/63-hh-ex3-term.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron --set ana.apron.domain polyhedra --enable ana.apron.strengthening --set ana.activated[+] unassume --set witness.yaml.unassume 63-hh-ex3-term.yml --enable ana.widen.tokens --disable witness.invariant.other --enable exp.arg.enabled
+// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron --set ana.apron.domain polyhedra --enable ana.apron.strengthening --set witness.yaml.entry-types[*] location_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 63-hh-ex3-term.yml --enable ana.widen.tokens --disable witness.invariant.other --enable exp.arg.enabled
 extern void __assert_fail (const char *__assertion, const char *__file,
       unsigned int __line, const char *__function)
      __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// PARAM: --enable ana.int.enums --set witness.yaml.validate 01-base-lor-enums.yml`
	`1`	`+// PARAM: --enable ana.int.enums --set witness.yaml.entry-types[*] location_invariant --set witness.yaml.validate 01-base-lor-enums.yml`
`2`	`2`
`3`	`3`	`int main() {`
`4`	`4`	`int r; // rand`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// PARAM: --set witness.yaml.validate 02-base-lor-addr.yml`
	`1`	`+// PARAM: --set witness.yaml.entry-types[*] location_invariant --set witness.yaml.validate 02-base-lor-addr.yml`
`2`	`2`
`3`	`3`	`int main() {`
`4`	`4`	`int r; // rand`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// SKIP PARAM: --set ana.base.privatization write+lock --enable ana.int.interval --set witness.yaml.validate 04-base-priv-sync-prune.yml`
	`1`	`+// SKIP PARAM: --set ana.base.privatization write+lock --enable ana.int.interval --set witness.yaml.entry-types[*] location_invariant --set witness.yaml.validate 04-base-priv-sync-prune.yml`
`2`	`2`	`// TODO: fix unsoundness in base priv syncs`
`3`	`3`	`#include <pthread.h>`
`4`	`4`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// PARAM: --enable ana.int.interval --set witness.yaml.validate 07-base-lor-interval.yml`
	`1`	`+// PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] location_invariant --set witness.yaml.validate 07-base-lor-interval.yml`
`2`	`2`	`#include <goblint.h>`
`3`	`3`
`4`	`4`	`int main() {`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.activated[+] unassume --set witness.yaml.unassume 10-apron-unassume-interval.yml`
	`1`	`+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 10-apron-unassume-interval.yml`
`2`	`2`	`#include <assert.h>`
`3`	`3`	`// Using polyhedra instead of octagon, because the former has no narrowing and really needs the witness.`
`4`	`4`	`int main() {`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 11-base-unassume-interval.yml`
	`1`	`+// SKIP PARAM: --enable ana.int.interval --set witness.yaml.entry-types[*] loop_invariant --set ana.activated[+] unassume --set witness.yaml.unassume 11-base-unassume-interval.yml`
`2`	`2`	`#include <assert.h>`
`3`	`3`
`4`	`4`	`int main() {`