Trivial overapproximation with true when SMT formula cannot be turned into C formula
When generating witnesses for predicate analysis, the class FormulaToCVisitor
is used to transform an overapproximation of the state from an AbstractionFormula
into an ExpressionTree
. For some tasks this fails due to unsupported operations, which returns the trivial overapproximation True
as seen here. Due to this some witnesses contain no/only trivial invariants.
A concrete example can be seen with the following command line:
scripts/cpa.sh -svcomp24 -heap 10000M -benchmark -timelimit '900 s' -stats -spec ../../sv-benchmarks/c/properties/unreach-call.prp -64 ../../sv-benchmarks/c/hardware-verification-bv/btor2c-lazyMod.cal10.c -setprop cpa.arg.exportYAMLCorrectnessWitnessesDirectlyFromARG=true
Where the transformation fails due to BV_ZERO_EXTENSION
being unsupported in the FormulaToCVisitor
.