(rewriter.flat=false) Invalid model on QF_SLIA formula

[muchang]

Hi,
For this case, Z3 release gives an invalid model:

[514] % cvc4 --strings-exp -q small.smt2
sat
[515] % z3release small.smt2
unknown
[516] % z3-4.8.7 small.smt2
unknown
[517] % z3-4.8.7 rewriter.flat=false model_validate=true small.smt2
sat
[518] % z3release rewriter.flat=false model_validate=true small.smt2
sat
(error "line 7 column 10: an invalid model was generated")
[519] % 
[519] % cat small.smt2
(declare-fun a () String)
(declare-fun b () Int)
(assert (xor (= (str.replace "A" (int.to.str b) a) (str.++ "A" (str.replace "" (int.to.str b) a)))
     (= (str.replace a (str.at a b) "")
     (str.++ (str.replace (str.substr a b 27)
          (str.substr a b 9) "") (str.substr a 5 (str.len a))))))
(check-sat)
[520] %

OS: Ubuntu 18.04
Commit: bcbe802

[NikolajBjorner]

duplicate