From ea98a330aa0109227bf1e266dad910feae81cf93 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 6 May 2024 15:52:19 +0200
Subject: [PATCH] Let arbitrary boolean values used in MaySet encoding depend
 on reference

---
 src/nagini_translation/translators/common.py   | 6 +++---
 src/nagini_translation/translators/contract.py | 2 +-
 src/nagini_translation/translators/program.py  | 3 ++-
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/nagini_translation/translators/common.py b/src/nagini_translation/translators/common.py
index 9660d35d..b6075359 100644
--- a/src/nagini_translation/translators/common.py
+++ b/src/nagini_translation/translators/common.py
@@ -921,15 +921,15 @@ def get_fresh_int_lit(self, ctx: Context) -> Expr:
         return self.viper.IntLit(ctx.get_fresh_int(), self.no_position(ctx),
                                  self.no_info(ctx))
 
-    def get_unknown_bool(self, ctx: Context) -> Expr:
+    def get_unknown_bool(self, arg: Expr, ctx: Context) -> Expr:
         """
-        Returns an arbitrary but fixed boolean value.
+        Returns an arbitrary but fixed boolean value that depends on the value of arg.
         """
         pos = self.no_position(ctx)
         info = self.no_info(ctx)
         fresh_int = self.get_fresh_int_lit(ctx)
         param = self.viper.LocalVarDecl('i', self.viper.Int, pos, info)
-        return self.viper.FuncApp(ARBITRARY_BOOL_FUNC, [fresh_int], pos, info,
+        return self.viper.FuncApp(ARBITRARY_BOOL_FUNC, [fresh_int, self.to_ref(arg, ctx)], pos, info,
                                   self.viper.Bool, [param])
 
     def _conjoin(self, eqs: List[Expr], pos: Position, info: Info) -> Expr:
diff --git a/src/nagini_translation/translators/contract.py b/src/nagini_translation/translators/contract.py
index 455f00d3..5c77a228 100644
--- a/src/nagini_translation/translators/contract.py
+++ b/src/nagini_translation/translators/contract.py
@@ -312,7 +312,7 @@ def translate_may_set(self, node: ast.Call, ctx: Context) -> StmtsAndExpr:
                                                 pos, info)
         result_ex = self.viper.CondExp(have_normal_perm, normal_acc, may_set_pred, pos,
                                        info)
-        unknown = self.get_unknown_bool(ctx)
+        unknown = self.get_unknown_bool(rec, ctx)
         result_in = self.viper.CondExp(unknown, normal_acc, may_set_pred, pos, info)
         return [], self.viper.InhaleExhaleExp(result_in, result_ex, pos, info)
 
diff --git a/src/nagini_translation/translators/program.py b/src/nagini_translation/translators/program.py
index f2d25da7..63b80e85 100644
--- a/src/nagini_translation/translators/program.py
+++ b/src/nagini_translation/translators/program.py
@@ -688,7 +688,8 @@ def create_arbitrary_bool_func(self, ctx: Context) -> 'silver.ast.Function':
         pos = self.no_position(ctx)
         info = self.no_info(ctx)
         i_param_decl = self.viper.LocalVarDecl('i', self.viper.Int, pos, info)
-        return self.viper.Function(ARBITRARY_BOOL_FUNC, [i_param_decl],
+        r_param_decl = self.viper.LocalVarDecl('r', self.viper.Ref, pos, info)
+        return self.viper.Function(ARBITRARY_BOOL_FUNC, [i_param_decl, r_param_decl],
                                    self.viper.Bool, [], [], None, pos, info)
 
     def create_may_set_predicate(self, ctx: Context) -> 'silver.ast.Predicate':