Repeated Counterexample in PredicateAnalysis when using Princess with BV-encoding
The following cmdline reports a repeated counterexample:
scripts/cpa.sh \
-setprop cpa.predicate.encodeBitvectorAs=BITVECTOR \
-setprop cpa.predicate.encodeFloatAs=INTEGER \
-predicateAnalysis -setprop solver.solver=PRINCESS -32 \
-spec ../sv-benchmarks/c/properties/unreach-call.prp \
../sv-benchmarks/c/loops-crafted-1/in-de61.c
As this task is quite simple, there might be a deeper bug, e.g.,
problems in the interpolation procedure of Princess when using bitvectors.
The same issue appears for half of the Reachsafety-Loops
category.