Hi,
For this case, Z3 gives an invalid model:
[670] % z3release model_validate=true small.smt2
sat
[671] % z3release smt.arith.solver=2 model_validate=true small.smt2
sat
(error "line 5 column 10: an invalid model was generated")
[672] %
[672] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () String)
(declare-fun c () String)
(assert (str.<= "ABCD" (str.++ b (int.to.str a) c)))
(check-sat)
[673] %
OS: Ubuntu 18.04
Commit: e1fa04b
Hi,
For this case, Z3 gives an invalid model:
OS: Ubuntu 18.04
Commit: e1fa04b