Fix relational witness literature examples to also validate

goblint · Aug 1, 2023 · c722f02 · c722f02
1 parent f5a1641
commit c722f02
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
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 --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 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/37-hh-ex3.yml b/tests/regression/56-witness/37-hh-ex3.yml
@@ -20,10 +20,10 @@
   location:
     file_name: 37-hh-ex3.c
     file_hash: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
-    line: 7
+    line: 6
     column: 4
     function: main
   location_invariant:
-    string: 0 <= i && i <= 3 && j == 0
+    string: 0 <= i && i <= 3
     type: assertion
     format: C
diff --git a/tests/regression/56-witness/40-bh-ex1-poly.yml b/tests/regression/56-witness/40-bh-ex1-poly.yml
@@ -20,10 +20,10 @@
   location:
     file_name: 40-bh-ex1-poly.c
     file_hash: 34f781dcae089ecb6b7b2811027395fcb501b8477b7e5016f7b38081724bea28
-    line: 8
+    line: 7
     column: 4
     function: main
   location_invariant:
-    string: 0 <= i && i <= 3 && j == 0
+    string: 0 <= i && i <= 3
     type: assertion
     format: C