Analyze time for transfer relation in Fuzzle benchmarks
When we run the following command line with 1h of time limit, we get the below statistics (shortened):
bin/cpachecker --heap 10000M --timelimit 1h --no-output-files --svcomp25 --stats --spec test/programs/benchmarks/properties/unreach-call.prp --64 test/programs/benchmarks/fuzzle-programs/05_fuzzle_70x70.c
PredicateCPA statistics
-----------------------
Time for post operator: 1.908s
Time for path formula creation: 1.891s
Time for strengthen operator: 0.060s
Time for prec operator: 0.050s
Time for abstraction: 0.001s (Max: 0.001s, Count: 1)
Solving time: 0.000s (Max: 0.000s)
Model enumeration time: 0.000s
Time for BDD construction: 0.000s (Max: 0.000s)
Time for merge operator: 13.778s
Time for coverage checks: 0.002s
Total time for SMT solver (w/o itp): 0.000s
ValueAnalysisCPA statistics
---------------------------
Time for transfer relation: 1.410s
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Total time for successor computation: 0.057s
CPA algorithm statistics
------------------------
Total time for CPA algorithm: 781.546s (Max: 781.546s)
Time for choose from waitlist: 0.089s
Time for precision adjustment: 3.072s
Time for transfer relation: 763.041s
Time for merge operator: 14.728s
Time for stop operator: 0.255s
Time for adding to reached set: 0.211s
Only BMC is executed, and we can see that the time for the transfer relation was 763s. However, the time measurements for the transfer relations of the PredicateCPA, ValueAnalysisCPA, and AutomatonCPA are all below 2s each.
The full list of used CPAs is this:
cpa.arg.ARGCPA
cpa.location.LocationCPA
cpa.callstack.CallstackCPA
cpa.functionpointer.FunctionPointerCPA
cpa.predicate.PredicateCPA
cpa.assumptions.storage.AssumptionStorageCPA
cpa.loopbound.LoopBoundCPA
cpa.value.ValueAnalysisCPA
We need to investigate which of these takes so much time.