From 2b6e5dcf1f5db7284b6f22faa3d1465df6bc2a93 Mon Sep 17 00:00:00 2001
From: Tom Rousseaux <rousseaux1.linerider@gmail.com>
Date: Wed, 30 Mar 2022 15:56:43 +0200
Subject: [PATCH] inlining functions with seahorn

---
 src/pv/verifiers/seahorn/seahorn.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/pv/verifiers/seahorn/seahorn.sh b/src/pv/verifiers/seahorn/seahorn.sh
index 9b0719c..db0906b 100755
--- a/src/pv/verifiers/seahorn/seahorn.sh
+++ b/src/pv/verifiers/seahorn/seahorn.sh
@@ -1,3 +1,3 @@
 #! /bin/sh
 
-sea bpf --cpu=1800 -g --bmc="${BMC}" --crab --track=mem --dsa=sea-cs -m64 -DPROVERS -DPROVERS_SEAHORN /mount/${1}/${2}.c
+sea bpf --cpu=1800 -g --bmc="${BMC}" --crab --track=mem --inline --dsa=sea-cs -m64 -DPROVERS -DPROVERS_SEAHORN /mount/${1}/${2}.c