Added lhs conjunct to avoid matching loop (#885)

viperproject · Dec 19, 2024 · 03e7dab · 03e7dab
1 parent 3e47ae2
commit 03e7dab
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/main/resources/dafny_axioms/sequences.vpr b/src/main/resources/dafny_axioms/sequences.vpr
@@ -123,7 +123,7 @@ domain $Seq[E] {
     axiom {
         forall s: $Seq[E], t: $Seq[E], 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))))
     }
     axiom {
         forall s: $Seq[E], t: $Seq[E], n: Int ::