Can CPAchecker take a set of predicates as input?

[Yoel Kim]

Dear developers of CPAchecker,

I'm trying to apply predicates extracted from other tools, not from CPAchecker's interpolation process. 

The problem I'm wondering about is whether CPAchecker can automatically calculate the predicate, such as (x == y), provided to the loop head L4  (please check page 22, https://www.sosy-lab.org/research/prs/Latest_UnifyingViewSmtBasedSoftwareVerification.pdf), within SSA form, eventually generating the coressponding SMT formula.

What I understand is that predicates derived from interpolation are already in the form of SMT formulas. However, what I want to do is provide predicates at the code level.

Regards
Yoel