Investigate CVC5 SEGFAULTs in CPAchecker

[baierd]

CVC5 SEGFAULTs in CPAchecker on the JavaSMT 6.0.0 update branch (here) sometimes (but consistently), for example for the following command line bin/cpachecker --option cpa.arg.compressWitness=true --option counterexample.export.compressWitness=true --option termination.compressWitness=true --svcomp26 --heap 10000M --benchmark --timelimit '900 s' --option solver.solver=cvc5 --stats --spec test/programs/benchmarks/properties/termination.prp --64 test/programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--media--common--tuners--tda18218.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i.

We should look into this.

More examples can be found here:
termination.results.2026-04-09_10-59-29.table.html

[baierd]

More cases can be found here:
overflow.results.2026-04-09_10-24-49.table.html.

[daniel-raffler]

I tried your command and it crashes without a stacktrace in the log:

Running CPAchecker with default stack size (1024k). Specify a larger value with --stack if needed.
Detected property termination and switching to config file config/svcomp26--termination.properties (CPAMain.createNewConfigForSwitching, INFO)

Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 4.2.2-884-g310b5e9ba9+ (OpenJDK 64-Bit Server VM 21.0.10) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "test/programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--media--common--tuners--tda18218.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i" (CPAchecker.parse, INFO)

Dead code detected: Label switch_break is not reachable. (CFAFunctionBuilder.leave, INFO)

line 5129: Function pointer *__cil_tmp221 with type int (*)(struct dvb_frontend *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 4977: Function pointer *__cil_tmp148 with type int (*)(struct dvb_frontend *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 4488: Function pointer *__cil_tmp34 with type int (*)(struct dvb_frontend *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 4460: Function pointer *__cil_tmp17 with type int (*)(struct dvb_frontend *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 4240: Function pointer *__cil_tmp268 with type int (*)(struct dvb_frontend *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 4025: Function pointer *__cil_tmp141 with type int (*)(struct dvb_frontend *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 4384: Function pointer *__cil_tmp38 with type int (*)(struct dvb_frontend *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

line 4352: Function pointer *__cil_tmp17 with type int (*)(struct dvb_frontend *, int) is called, but no possible target functions were found. (CFunctionPointerResolver.getTargets, WARNING)

Using Restarting Algorithm (CoreComponentsFactory.createAlgorithm, INFO)

The following configuration options were specified but are not used:
 cpa.arg.lateMerge
 solver.solver
 counterexample.export.exportWitness
 cpa.arg.compressWitness
 counterexample.export.compressWitness
 termination.compressWitness 
 (CPAchecker.printConfigurationWarnings, WARNING)

Starting analysis ... (CPAchecker.runAlgorithm, INFO)

Loading analysis 1 from file config/components/svcomp26--parallel-termination.properties ... (RestartAlgorithm.run, INFO)

Using the following resource limits: CPU-time limit of 900s (Analysis config/components/svcomp26--parallel-termination.properties:ResourceLimitChecker.fromConfiguration, INFO)

Mismatch of configuration options when loading from 'config/components/svcomp26--termination-terminationToSafety.properties': 'analysis.algorithm.termination' has two values 'true' and 'false'. Using 'false'. (Analysis config/components/svcomp26--parallel-termination.properties:NestingAlgorithm.checkConfigs, INFO)

Mismatch of configuration options when loading from 'config/components/svcomp26--termination-terminationToSafety.properties': 'cpa.arg.compressWitness' has two values 'true' and 'false'. Using 'false'. (Analysis config/components/svcomp26--parallel-termination.properties:NestingAlgorithm.checkConfigs, INFO)

Using the following resource limits: CPU-time limit of 900s, Thread CPU-time limit of 300s (Analysis config/components/svcomp26--parallel-termination.properties:Parallel analysis config/components/svcomp26--termination-terminationToSafety.properties:ResourceLimitChecker.fromConfiguration, INFO)

Using predicate analysis with CVC5 1.3.4.dev+main@d22638a. (Analysis config/components/svcomp26--parallel-termination.properties:Parallel analysis config/components/svcomp26--termination-terminationToSafety.properties:PredicateCPA:PredicateCPA.<init>, INFO)

Mismatch of configuration options when loading from 'config/components/svcomp26--termination-lassoBasedAnalysis.properties': 'termination.compressWitness' has two values 'true' and 'false'. Using 'false'. (Analysis config/components/svcomp26--parallel-termination.properties:NestingAlgorithm.checkConfigs, INFO)

Using the following resource limits: CPU-time limit of 900s (Analysis config/components/svcomp26--parallel-termination.properties:Parallel analysis config/components/svcomp26--termination-lassoBasedAnalysis.properties:ResourceLimitChecker.fromConfiguration, INFO)

Using predicate analysis with CVC5 1.3.4.dev+main@d22638a and JFactory 1.21. (Analysis config/components/svcomp26--parallel-termination.properties:Parallel analysis config/components/svcomp26--termination-lassoBasedAnalysis.properties:PredicateCPA:PredicateCPA.<init>, INFO)

Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (Analysis config/components/svcomp26--parallel-termination.properties:Parallel analysis config/components/svcomp26--termination-lassoBasedAnalysis.properties:PredicateCPA:PredicateCPARefiner.<init>, INFO)

Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics. (Analysis config/components/svcomp26--parallel-termination.properties:Parallel analysis config/components/svcomp26--termination-lassoBasedAnalysis.properties:FormulaManagerView.<init>, WARNING)

Starting analysis 1 ... (RestartAlgorithm.run, INFO)

Starting termination algorithm. (Analysis config/components/svcomp26--parallel-termination.properties:Parallel analysis config/components/svcomp26--termination-lassoBasedAnalysis.properties:TerminationAlgorithm.run0, INFO)

line 4025: Ignoring call via function pointer tda18218_set_params::__cil_tmp141 for which no suitable target was found in line: (*__cil_tmp141)(fe, 1); (Analysis config/components/svcomp26--parallel-termination.properties:Parallel analysis config/components/svcomp26--termination-lassoBasedAnalysis.properties:FunctionPointerCPA:FunctionPointerTransferRelation.getAbstractSuccessorsForEdge, WARNING)

line 4025: Ignoring function call through function pointer *__cil_tmp141: (*__cil_tmp141)(fe, 1); (Analysis config/components/svcomp26--parallel-termination.properties:Parallel analysis config/components/svcomp26--termination-lassoBasedAnalysis.properties:PredicateCPA:ExpressionToFormulaVisitor.visit, WARNING)

Limiting unrolling of non-literal-length slice assignment to 20, soundness may be lost (Analysis config/components/svcomp26--parallel-termination.properties:Parallel analysis config/components/svcomp26--termination-lassoBasedAnalysis.properties:PredicateCPA:AssignmentQuantifierHandler.unrollQuantifier, WARNING)

Segmentation fault (core dumped)

This usually means there's a stack overflow, and adding something like --stack 50M seems to fix the crash. Could you upload the log files for the other runs? Or maybe just repeat them with a larger stack size