Set paths-symex-explore-all when unwinding-assertions defaults to true

tautschnig · tautschnig · commit bc8cdc9645ec · 2026-03-13T09:42:05.000Z
When unwinding-assertions is enabled by default (via
set_default_analysis_flags), paths-symex-explore-all must also be
enabled. Otherwise, the single-path symex checker's
has_finished_exploration check can return true before any path is
explored, because dynamically generated properties (like 'no body for
callee') don't exist in the initial properties map.

The explicit --unwinding-assertions flag already set
paths-symex-explore-all (line 192), but the default enablement path
did not, causing --paths lifo to miss no-body assertions.

Co-authored-by: Kiro &lt;kiro-agent@users.noreply.github.com&gt;

All 19 tests previously tagged paths-lifo-expected-failure now pass,
so remove the tag and the corresponding exclusion from the Makefile
and CMakeLists.txt.
diff --git a/regression/cbmc/Array_operations4/program-only.desc b/regression/cbmc/Array_operations4/program-only.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 main.c
 --program-only
 target!0@1#2 ==
diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
@@ -13,7 +13,7 @@ add_test_pl_tests(
 add_test_pl_profile(
     "cbmc-paths-lifo"
     "$<TARGET_FILE:cbmc> --paths lifo"
-    "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo"
+    "-C;-X;thorough-paths;-X;smt-backend;${gcc_only_string}-s;paths-lifo"
     "CORE"
 )
 
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
@@ -26,7 +26,7 @@ test-z3:
 
 test-paths-lifo:
 	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \
-					  -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
+					  -X thorough-paths -X smt-backend \
 					  -s paths-lifo $(GCC_ONLY)
 
 test-new-smt-backend:
diff --git a/regression/cbmc/array-cell-sensitivity15/test.desc b/regression/cbmc/array-cell-sensitivity15/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 access.c
 --program-only
 ^EXIT=0$
diff --git a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --cover location --pointer-check --malloc-may-fail --malloc-fail-null
 \[main\.coverage\.5\] file test\.c line \d+ function main block 5 \(lines test\.c:main:17,18\): SATISFIED
diff --git a/regression/cbmc/cover-failed-assertions/test.desc b/regression/cbmc/cover-failed-assertions/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --cover location --cover-failed-assertions --malloc-may-fail --malloc-fail-null
 \[main.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED
diff --git a/regression/cbmc/fault_localization-stop_on_fail1/test.desc b/regression/cbmc/fault_localization-stop_on_fail1/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure broken-smt-backend no-new-smt
+CORE broken-smt-backend no-new-smt
 main.c
 --localize-faults --stop-on-fail --no-standard-checks
 ^EXIT=10$
diff --git a/regression/cbmc/outfile_no_dir/test.desc b/regression/cbmc/outfile_no_dir/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 main.c
 --dimacs --outfile /xyz/out.dimacs
 ^EXIT=1$
diff --git a/regression/cbmc/residual-guards-1/test.desc b/regression/cbmc/residual-guards-1/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --show-vcc --unwind 10
 ^\{1\} main::argc!0@1#1 = 1$
diff --git a/regression/cbmc/residual-guards-2/test.desc b/regression/cbmc/residual-guards-2/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --show-vcc --unwind 10
 ^\{1\} main::argc!0@1#1 = 1$
diff --git a/regression/cbmc/residual-guards-3/test.desc b/regression/cbmc/residual-guards-3/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --show-vcc --depth 1000
 ^\{1\} main::argc!0@1#1 = 1$
diff --git a/regression/cbmc/residual-guards-4/test.desc b/regression/cbmc/residual-guards-4/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --show-vcc
 ^\{1\} main::argc!0@1#1 = 1$
diff --git a/regression/cbmc/sat-solver-error/test.desc b/regression/cbmc/sat-solver-error/test.desc
@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend broken-cprover-smt-backend paths-lifo-expected-failure no-new-smt
+CORE broken-z3-smt-backend broken-cprover-smt-backend no-new-smt
 test.c
 --sat-solver non-existing-solver
 ^EXIT=1$
diff --git a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc b/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --function test --show-vcc
 ^EXIT=0$
diff --git a/regression/cbmc/symex_should_filter_value_sets/test.desc b/regression/cbmc/symex_should_filter_value_sets/test.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 main.c
 --show-vcc
 ^EXIT=0$
diff --git a/regression/cbmc/unreachable-goto1/test-vccs.desc b/regression/cbmc/unreachable-goto1/test-vccs.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --show-vcc --verbosity 8
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/regression/cbmc/unreachable-goto2/test-vccs.desc b/regression/cbmc/unreachable-goto2/test-vccs.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --show-vcc --verbosity 8
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/regression/cbmc/unreachable-goto3/test-vccs.desc b/regression/cbmc/unreachable-goto3/test-vccs.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --show-vcc --verbosity 8
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/regression/cbmc/unreachable-goto4/test-vccs.desc b/regression/cbmc/unreachable-goto4/test-vccs.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --show-vcc --verbosity 8
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/regression/cbmc/unreachable-goto5/test-vccs.desc b/regression/cbmc/unreachable-goto5/test-vccs.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --show-vcc --verbosity 8
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/regression/cbmc/unreachable-goto6/test-vccs.desc b/regression/cbmc/unreachable-goto6/test-vccs.desc
@@ -1,4 +1,4 @@
-CORE paths-lifo-expected-failure
+CORE
 test.c
 --show-vcc --verbosity 8
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -125,6 +125,7 @@ void cbmc_parse_optionst::set_default_analysis_flags(
   if(!options.is_set("unwinding-assertions"))
   {
     options.set_option("unwinding-assertions", enabled);
+    options.set_option("paths-symex-explore-all", enabled);
   }
 
   if(enabled)

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE paths-lifo-expected-failure`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`	`--program-only`
`4`	`4`	`target!0@1#2 ==`
Original file line number	Diff line number	Diff line change
`@@ -13,7 +13,7 @@ add_test_pl_tests(`
`13`	`13`	`add_test_pl_profile(`
`14`	`14`	`"cbmc-paths-lifo"`
`15`	`15`	`"$<TARGET_FILE:cbmc> --paths lifo"`
`16`		`- "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo"`
	`16`	`+ "-C;-X;thorough-paths;-X;smt-backend;${gcc_only_string}-s;paths-lifo"`
`17`	`17`	`"CORE"`
`18`	`18`	`)`
`19`	`19`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE paths-lifo-expected-failure broken-smt-backend no-new-smt`
	`1`	`+CORE broken-smt-backend no-new-smt`
`2`	`2`	`main.c`
`3`	`3`	`--localize-faults --stop-on-fail --no-standard-checks`
`4`	`4`	`^EXIT=10$`