Ultimate TestGen: Combining Parallel Trace Abstraction and Symbolic Path Execution (Competition Contribution)

Abstract Prior to Test-Comp 2026, Ultimate TestGengenerated test cases with a sequential software model checking approach, which is named trace abstraction and performs counterexample-guided abstraction refinement. To generate tests, Ultimate TestGenencodes test goals as property violations and generates test cases from counterexamples detected by trace abstraction.For Test-Comp 2026, we keep this general principle but make two changes.First, we adapt Ultimate TestGento a recent parallelization of trace abstraction.Second, we extend Ultimate TestGenwith a Path-Checker, which runs in parallel with parallel trace abstraction and exhaustively explores counterexamples but skips refinement.