Is it possible to add Path satisfaction analysis to SVF?

[spingARbor]

Hi, sir When I test leak checker of SVF in Juliet,I found SVF produced many false alarms when checking cases as following: if(condition) molloc() if(condition) free() (The case molloc and free in the same condition.) And,SVF also doesn't determine if the leak path is practicable.So,I'd like to consult if there is any work or try that add Path satisfaction analysis to SVF. Thank you!