Witness Export takes >900s
CPAchecker is able to solve ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--vfio--pci--vfio-pci.ko-entry_point.cil.out.i
from sv-benchmarks in about 20 seconds. Afterwards, the witness export does not finish within 15 minutes. The reached set contains 550,000 abstract states after the analysis finishes which probably is the root cause of the problem. Is there a way to speed-up the export?
Command to reproduce:
scripts/cpa.sh -valueAnalysis -stats -spec sv-benchmarks/c/properties/unreach-call.prp -64 sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--vfio--pci--vfio-pci.ko-entry_point.cil.out.i
Edited by Matthias Kettl