Missed non-negativity of `str.len`

[maurobringolf]

Commit: 2138ef2

I would expect (<= 0 (str.len _)) to be equivalent to true, but here it results in a completeness regression:

$ z3-4.8.10 unknown.smt2
unsat
$ z3trunk unknown.smt2
unknown
$ cat unknown.smt2
(declare-const x Int)
(assert (forall ((V Int)) (or (= 0 V) (not (<= 0 (str.len (str.substr "HySXCWhAK" x 1)))))))
(check-sat)

$ z3-4.8.10 unknown.smt2
unsat
$ z3trunk unknown.smt2
unsat
$ cat unknown.smt2
(declare-const x Int)
(assert (forall ((V Int)) (or (= 0 V) (not true))))
(check-sat)

[NikolajBjorner]

I currently don't simplify (<= 0 (str.len xx)) away because the string theory needs to create these as axioms to the arithmetic solver and these axioms get rewritten. This was in fact a regression when attempting to add such simplifications.