When does predicate analysis construct correctness witnesses with invariants?

Hi all,

I noticed that predicate analysis sometimes produces correctness witnesses without any invariants. What is necessary for predicate analysis to produce a witness with invariants?

For example:

scripts/cpa.sh -predicateAnalysis \
    -setprop cpa.arg.proofWitness=witness.graphml \
    -setprop cpa.arg.compressWitness=false \
    ../../sv-benchmarks/c/loop-invariants/const.c

with program const.c produces a correctness witness without any invariants.

A valid invariant to prove const.c true for property unreach-call (VERIFIER_error) is s == 0, and the predicate analysis also uses this predicate (last line in the output below):

❱ cat output/predmap.txt
(set-info :source |printed by MathSAT|)
(declare-fun |__VERIFIER_assert::cond| () (_ BitVec 32))
(declare-fun |main::s| () (_ BitVec 32))

__VERIFIER_assert:
(assert (let ((.def_65 (= |__VERIFIER_assert::cond| (_ bv0 32)))).def_65))

__VERIFIER_assert N5:
(assert false)
(assert (let ((.def_65 (= |__VERIFIER_assert::cond| (_ bv0 32)))).def_65))

main N12:
(assert (let ((.def_87 (= |main::s| (_ bv0 32)))).def_87))

I know that just because some predicate is used does not mean that this predicate is an invariant, but I'm still curious about what the difficulty is here.

Thanks for any insights!