Can Seahorn treat a function as pure?

[rcdickerson]

Hello! I'm looking for a way to get Seahorn to treat a function as pure. For example, I would like this to verify under the assumption that x == y => f(x) == f(y):

#include "seahorn/seahorn.h"
extern int f(int);

void main(void) {
  int x = f(5);
  int y = f(5);
  sassert(x == y);
 }

I'm essentially looking for a way to have the verifier treat f as a vanilla EUF function. Is there a way to ask Seahorn to treat a function this way, or otherwise encode this kind of assumption about f?

[agurfinkel]

the bmc engine has an option for that. We have not used it in a while, so it might need some improvements. It does work for your specific example:

./run/bin/sea bpf -S -m64 --bmc=opsem  /tmp/issue538.c --horn-bv2-enable-external-calls
...
Modelling   %_0 = tail call i32 @f(i32 noundef 5) #7 with an uninterpreted function
Modelling   %_1 = tail call i32 @f(i32 noundef 5) #7 with an uninterpreted function
unsat