From b1d5d61b9c0601a1fcaab683bf59ff35e5bf6709 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 9 Oct 2023 22:47:37 +0200
Subject: [PATCH] Fixing computation of constrainable terms

---
 src/main/scala/state/Terms.scala | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala
index bdeae6a99..966f306fd 100644
--- a/src/main/scala/state/Terms.scala
+++ b/src/main/scala/state/Terms.scala
@@ -2512,6 +2512,8 @@ object utils {
     case PermIntDiv(t0, _) => consumeExactRead(t0, constrainableARPs)
     case PermPermDiv(t0, t1) => consumeExactRead(t0, constrainableARPs) && consumeExactRead(t1, constrainableARPs)
     case PermMin(t0 ,t1) => consumeExactRead(t0, constrainableARPs) || consumeExactRead(t1, constrainableARPs)
+    case Ite(_, t0, NoPerm) => consumeExactRead(t0, constrainableARPs)
+    case Ite(_, NoPerm, t1) => consumeExactRead(t1, constrainableARPs)
     case Ite(_, t0, t1) => consumeExactRead(t0, constrainableARPs) || consumeExactRead(t1, constrainableARPs)
     case _ => true
   }