Literal strings in a function call fails a length refinement

[briangmilnes]

module LiteralStringRefBug

open FStar.String

let replacePrefix (pre: string) (s: string{length pre <= length s}) (wth: string) : Tot string = s

let invalidAbbreviations confs = replacePrefix "<HOME>" "<HOME>/bin/fstar.exe" "/usr/mlnes"

the second string is failing on the length refinement. if length tests before it allows it to pass.

So something must be a bit funky in what Z3 is getting wrt literal strings.