From e343873bbb2c827bc63decde6331df58dd0b7493 Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Thu, 5 Dec 2024 23:28:53 +0100
Subject: [PATCH] Added lhs conjunct to avoid matching loop

---
 .../impls/sequence_axioms/SequenceAxiomatization.scala        | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala b/src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala
index 469fd82d..685a196b 100644
--- a/src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala
+++ b/src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala
@@ -31,6 +31,7 @@ object SequenceAxiomatization {
                 | // diff 13 implemented, for now (may reduce completeness, but there's a known matching loop when the first drop amount is 0); another option would be to add !=0 as an explicit condition
                 | // diff 14 implemented: eliminate index over take/drop for trivial cases (to avoid matching loops when e.g. s[i..] == s is known)
                 | // diff 16 implemented: remove general cases of equality-learning between take/drop/append subsequences; only allow when take/drop are at top level (this affects linkedlists test case)
+                | // diff 17: removing a potential matching loop where more than one axiom applies to a Seq#Take(Seq#Append(s,t),n) term
                 |// START BASICS
                 |type Seq T;
                 |
@@ -189,9 +190,10 @@ object SequenceAxiomatization {
                 |  { Seq#Take(Seq#Append(s,t),n) } //{Seq#Append(s,t), Seq#Take(s,n)} // diff 16: temporarily dropped general case of these
                 |  0 < n && n <= Seq#Length(s) ==> Seq#Take(Seq#Append(s,t),n) == Seq#Take(s,n));
                 |
+                |// diff 17: added a conjunct on the lhs of the implication
                 |axiom (forall<T> s: Seq T, t: Seq T, n:int ::
                 |  { Seq#Take(Seq#Append(s,t),n) }
-                |  n > 0 && n > Seq#Length(s) ==> Seq#Add(Seq#Sub(n,Seq#Length(s)),Seq#Length(s)) == n && Seq#Take(Seq#Append(s,t),n) == Seq#Append(s,Seq#Take(t,Seq#Sub(n,Seq#Length(s)))));
+                |  n > 0 && n > Seq#Length(s) && n < Seq#Length(Seq#Append(s,t)) ==> Seq#Add(Seq#Sub(n,Seq#Length(s)),Seq#Length(s)) == n && Seq#Take(Seq#Append(s,t),n) == Seq#Append(s,Seq#Take(t,Seq#Sub(n,Seq#Length(s)))));
                 |
                 |// diff 16: temporarily dropped general case of these
                 |//axiom (forall<T> s: Seq T, t: Seq T, m:int ::