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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information