SMT translation of unknown values incorrect

[FliegendeWurst]

Description

It is is possible to prove the following using Z3:

 \forall Seq s; s = seqDef{int u;}(0, s.length, s[u]),
 seqSub(s1, 0, maxx - 1).length = maxx - 1
==>
 s1.length = maxx - 1

Equivalent .key:

\functions {
  Seq s1;
  int maxx;
}

\problem {
  \forall Seq s; (s = (seqDef{int u;}(0, s.length, any::seqGet(s, u))))
  & seqLen(seqSub(s1, 0, maxx - 1)) = maxx - 1
 ->
  s1.length = maxx - 1
}

Additional information

This is the relevant part of the SMT translation:

; --- Sequent
(assert
  (!
    (forall ((var_s U)) (=> (instanceof var_s sort_Seq) (= var_s unknown_0)))
    :named
    L_1))
(assert
  (!
    (=
      (k_seqLen (k_seqSub u_s1 (i2u 0) (i2u (- (u2i u_maxx) 1))))
      (i2u (- (u2i u_maxx) 1)))
    :named
    L_2))
(assert
  (! (not (= (k_seqLen u_s1) (i2u (- (u2i u_maxx) 1)))) :named L_3))
(check-sat)
; --- Translation of unknown values
; unknown_0 :  seqDef{u:int}(Z(0(#)),seqLen(s),any::seqGet(s,u))

In particular I think this allows the SMT solver to prove seqSub(s1, 0, maxx - 1) = unknown_0 = s1, which is obviously wrong.

cc @WolframPfeifer @mattulbrich

[WolframPfeifer]

Just for the fun: You can easily prove false as soon as you have at least to sequences that are not identical. The following can be proven instantly by SMT:

\functions {
  Seq s1;
  Seq s2;
}

\problem {
  \forall Seq s; (s = (seqDef{int u;}(0, s.length, any::seqGet(s, u))))
  & s1 != s2
 ->
  false
}

Note that the sub-formula with the universal quantifier is the formula introduced by the taclet seqSelfDefinition for any sequent.