cinvariants.export=true causes crash
CPAchecker crashed while I was experimenting with the cinvariants.export=true
option. Here is the command line I used:
scripts/cpa.sh -heap 10000M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -kInduction-kipdrdfInvariants -setprop cpa.invariants.useMod2Template=true -setprop cinvariants.export=true afnp2014_true-unreach-call.c.i
CPAchecker runs for a little less than a minute on my machine, outputting several messages in the process. At the end, it reports an exception, the first line of which is 'Exception in thread "main" java.lang.UnsupportedOperationException: Unexpected operand'. I have attached a file exception.txt that contains the full text of the exception. If I use the same command line without the cinvariants.export=true option, no exception appears, and CPAchecker terminates normally.
The file afnp2014_true-unreach-call.c.i is from SV-COMP’15. I got it directly from here: https://github.com/sosy-lab/sv-benchmarks/raw/svcomp15/c/loop-lit/afnp2014_true-unreach-call.c.i. Here are some details of my setup:
- CPAchecker: version 2.0
- Java: openjdk version "11.0.9.1" 2020-11-04
- OS: Ubuntu 18.04.5 LTS
- Platform: Linux x86_64
- RAM: 32 GB