From c7d46bab3cbad83ddb4ccc8564da9aadc17405c6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Sat, 21 Dec 2024 01:41:31 +0100
Subject: [PATCH] fix

---
 src/main/scala/viper/gobra/backend/ViperBackends.scala | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/main/scala/viper/gobra/backend/ViperBackends.scala b/src/main/scala/viper/gobra/backend/ViperBackends.scala
index 0a3510e2b..8ada26293 100644
--- a/src/main/scala/viper/gobra/backend/ViperBackends.scala
+++ b/src/main/scala/viper/gobra/backend/ViperBackends.scala
@@ -29,6 +29,7 @@ object ViperBackends {
       var options: Vector[String] = Vector.empty
       options ++= Vector("--logLevel", "ERROR")
       options ++= Vector("--disableCatchingExceptions")
+      options ++= Vector("--respectFunctionPrePermAmounts")
       if (config.conditionalizePermissions) {
         options ++= Vector("--conditionalizePermissions")
       }
@@ -84,6 +85,7 @@ object ViperBackends {
       if (config.assumeInjectivityOnInhale) {
         options ++= Vector("--assumeInjectivityOnInhale")
       }
+      options ++= Vector("--respectFunctionPrePermAmounts")
       options ++= exePaths
 
       new Carbon(options)
@@ -135,6 +137,7 @@ object ViperBackends {
       var options: Vector[String] = Vector.empty
       options ++= Vector("--logLevel", "ERROR")
       options ++= Vector("--disableCatchingExceptions")
+      options ++= Vector("--respectFunctionPrePermAmounts")
       // Gobra seems to be much slower with the new silicon axiomatization of collections.
       // For now, we stick to the old one.
       options ++= Vector("--useOldAxiomatization")
@@ -172,6 +175,7 @@ object ViperBackends {
     override def getViperVerifierConfig(exePaths: Vector[String], config: Config): ViperVerifierConfig = {
       var options: Vector[String] = Vector.empty
       options ++= Vector("--logLevel", "ERROR")
+      options ++= Vector("--respectFunctionPrePermAmounts")
       if (config.assumeInjectivityOnInhale) {
         options ++= Vector("--assumeInjectivityOnInhale")
       }