Fix expected test outcomes

Author: Remi Delmas

regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc

@@ -7,15 +7,22 @@ main.c
 ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
 ^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: FAILURE$
 ^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: FAILURE$
-^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: UNKNOWN$
 ^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: FAILURE$
 ^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: FAILURE$
 ^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: FAILURE$
-^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: UNKNOWN$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
+^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$
 --
 This test checks that when `__CPROVER_is_fresh` is disjunctions,
 the program accepts models where `__CPROVER_is_fresh` evaluates to false

regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/test.desc

@@ -2,15 +2,21 @@ CORE dfcc-only
 main.c
 --dfcc main --replace-call-with-contract foo
 ^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer NULL in \*x: FAILURE$
-^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*x: FAILURE$
+^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*x: UNKNOWN$
 ^\[bar.pointer_dereference.\d+\] line 24 dereference failure: deallocated dynamic object in \*x: FAILURE$
 ^\[bar.pointer_dereference.\d+\] line 24 dereference failure: dead object in \*x: FAILURE$
 ^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer outside object bounds in \*x: FAILURE$
-^\[bar.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*x: FAILURE$
+^\[bar.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*x: UNKNOWN$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
+^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer NULL in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 24 dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 24 dereference failure: dead object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*x: SUCCESS$
 --
 This test checks that when `__CPROVER_pointer_in_range_dfcc` is disjunctions,
 the program accepts models where `__CPROVER_pointer_in_range_dfcc` evaluates to