Invalid model for String formula (unsat_core, rewriter.elim_and, rewriter.local_ctx, smt.phase_selection)

[rainoftime]

Hi, for the following formula,

(set-option :model_validate true)
(set-option :unsat_core true)
(set-option :rewriter.elim_and true)
(set-option :rewriter.local_ctx true)
(set-option :smt.phase_selection 0)
(declare-const Str9 String)
(declare-const Str19 String)
(declare-const i7 Int)
(assert (>= (str.len Str9) i7))
(assert (>= (str.len (str.++ "" "fnmahu" Str19 (int.to.str (+ 884 518 796 0 i7)))) 38))
(assert (! true :named IP_2))
(check-sat)

z3 (commit dde0c51) gives an invalid model

[zhendongsu]

I guess the same here -- see Nikolaj's comment for https://github.com/Z3Prover/z3/issues/3902

[rainoftime]

lblpos and :named are different. The former one is introduced by Boogie, but :name is general in smt-lib2 (also supported by CVC4, OpenSMT, etc)

[rainoftime]

Fixed