(rewrite.flat=false) Invalid model returned

[jiwonparc]

commit: d9fb406

$ z3release model_validate=true bug.smt2
sat
( 
  (define-fun in1 () String
    "")
  (define-fun in0 () String
    "A")
)
$ z3release model_validate=true rewriter.flat=false bug.smt2
sat
(error "line 4 column 10: an invalid model was generated")
( 
  (define-fun in0 () String
    "")
  (define-fun in1 () String
    "")
)
$cat bug.smt2
(declare-fun in1 () String)
(declare-fun in0 () String)
(assert (not (= (ite (= (ite (= (str.len in0) 0) (ite (= (str.len in0) 0) 1 0) 0) (ite (and (and (and 
(not (not (= (ite (= (str.len in1) 1) 1 0) 0))) (not (not (= (ite (= (str.len in0) 0) 1 0) 0)))) 
(not (= (ite (= (str.len in0) 1) 1 0) (ite (= (str.len in0) 0) 1 0)))) 
(not (not (and (not (not (= (ite (= (str.len in1) 1) 1 0) 0))) 
(not (not (= (ite (= (str.len in1) 0) 1 0) 0))))))) 1 0)) 1 0) 0)))
(check-sat)
(get-model)

[wintered]

(rewriter.flat=false) Refutational soundness bug

commit: 04edfc9

• not necessarily related to the above but put it here to consolidate
• still quite sizable even after several reduction passes

$time z3release delta.out.smt2
sat
z3release delta.out.smt2  4.27s user 0.03s system 23% cpu 18.207 total
$time cvc4 --strings-exp -q delta.out.smt2
sat
cvc4 --strings-exp -q delta.out.smt2  1.84s user 0.05s system 24% cpu 7.711 total
$z3release rewriter.flat=false delta.out.smt2
unsat
$cat delta.out.smt2
(declare-fun uri () String)
(assert (and (and (and (and (and (= 0 (ite (str.contains (str.substr 
(str.substr uri 10 (- (str.len uri) 10)) 0 (str.indexof (str.substr uri 10 (- 
(str.len uri) 5)) "," 0)) "A") 1 0)) (= (ite (str.contains (str.substr 
(str.substr uri 10 (- (str.len uri) 10)) 0 (- (str.indexof (str.substr uri 10 
(- (str.len uri) 10)) "," 0) 0)) "C") 1 0) 0) (and (and (not (= (ite 
(str.contains (str.substr (str.substr uri 10 (- (str.len uri) 10)) 0 
(str.indexof (str.substr uri 10 (- (str.len uri) 10)) "," 0)) "N") 1 0) 0)) 
(not (and (and (and (and (and (not (not (= 0 (ite (str.contains (str.substr 
(str.substr uri 10 (- 10 (str.len uri))) 0 (str.indexof (str.substr uri 10 (- 
(str.len uri) 10)) "," 0)) "M") 1 0)))))) (= 0 (ite (str.contains (str.substr 
(str.substr uri 10 (- (str.len uri) 10)) 0 (str.indexof (str.substr uri 10 (- 
(str.len uri) 10)) "," 0)) "J") 1 0))))))) (not (not (= 0 (ite (str.contains 
(str.substr (str.substr uri 10 (- (str.len uri) 10)) 0 (- (str.indexof 
(str.substr uri 10 (- (str.len uri) 10)) "," 0) 0)) "L") 1 0))))) (not (not (= 
(ite (str.contains (str.substr (str.substr uri 10 (- (str.len uri) 10)) 0 (- 
(str.indexof (str.substr uri 10 (- (str.len uri) 10)) "," 0) 0)) "K") 1 0) 0))) 
(not (not (= (ite (str.contains (str.substr (str.substr uri 10 (- (str.len uri) 
10)) 0 (- (str.indexof (str.substr uri 10 (- (str.len uri) 10)) "," 0) 0)) "I") 
1 0) 0))) (not (not (= (ite (str.contains (str.substr (str.substr uri 10 (- 
(str.len uri) 10)) 0 (- (str.indexof (str.substr uri 10 (- (str.len uri) 10)) 
"," 0) 0)) "H") 1 0) 0))) (not (not (= (ite (str.contains (str.substr 
(str.substr uri 10 (- (str.len uri) 10)) 0 (- (str.indexof (str.substr uri 10 
(- (str.len uri) 10)) "," 0) 0)) "G") 1 0) 0))) (not (not (= (ite (str.contains 
(str.substr (str.substr uri 10 (- (str.len uri) 10)) 0 (- (str.indexof 
(str.substr uri 10 (- (str.len uri) 10)) "," 0) 0)) "F") 1 0) 0))) (not (not (= 
(ite (str.contains (str.substr (str.substr uri 10 (- (str.len uri) 10)) 0 
(str.indexof (str.substr uri 10 (- (str.len uri) 10)) "," 0)) "E") 1 0) 0)))) 
(not (not (= (ite (= (str.at (str.substr (str.substr uri 10 (- (str.len uri) 
10)) 0 (- (str.indexof (str.substr uri 10 (- (str.len uri) 10)) "," 0) 0)) 0) 
"[") 1 0) 0)))) (not (= (ite (not (= (str.len (str.substr (str.substr uri 10 (- 
(str.len uri) 10)) 0 (- (str.indexof (str.substr uri 10 (- (str.len uri) 10)) 
"," 0) 0))) 0)) 1 0) 0)) (not (not (= (ite (str.contains (str.substr 
(str.substr uri 10 (- (str.len uri) 10)) (+ (str.indexof (str.substr uri 10 (- 
(str.len uri) 10)) "," 0) 1) (- (str.len (str.substr uri 10 (- (str.len uri) 
10))) (+ 0 1))) ",") 1 0) 0))) (not (not (= (ite (= (str.len (str.substr 
(str.substr uri 10 (- (str.len uri) 10)) (+ (str.indexof (str.substr uri 10 (- 
(str.len uri) 10)) "," 0) 1) (- (str.len (str.substr uri 10 (- (str.len uri) 
10))) (+ (str.indexof (str.substr uri 10 (- (str.len uri) 10)) "," 0) 1)))) 0) 
1 0) 0))) (not (not (= (ite (str.contains (str.substr uri 10 (- (str.len uri) 
10)) "@") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr uri 10 (- 
(str.len uri) 10)) "?") 1 0) 0))) (not (not (= (ite (str.contains (str.substr 
uri 10 (- (str.len uri) 10)) "/") 1 0) 0))) (not (not (= (ite (str.contains 
(str.substr uri 10 (- (str.len uri) 10)) ".sock") 1 0) 0))) (not (= (ite (not 
(= (str.len (str.substr uri 10 (- (str.len uri) 10))) 0)) 1 0) 0)) (not (= (ite 
(str.prefixof "mongodb://" uri) 1 0) 0)) (>= (- (str.indexof (str.substr uri 10 
(- (str.len uri) 10)) "," 0) (ite (str.contains (str.substr (str.substr uri 10 
(- (str.len uri) 10)) 0 (- (str.indexof (str.substr uri 10 (- (str.len uri) 
10)) "," 0) 0)) "N") 1 0)) 0))))
(check-sat)