[776] % z3-4.8.8 small.smt2
sat
[777] % cvc4 --strings-exp -q small.smt2
sat
[778] % z3release small.smt2
unsat
[779] %
[779] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () String)
(assert (= a (- (str.len b) 10)))
(assert (str.contains (str.substr (str.substr b 10 a) 0 (- (str.indexof (str.substr b 10 a) "," 0) 0)) "M"))
(assert (= (ite (str.contains (str.substr (str.substr b 10 a) 0 (- (str.indexof (str.substr b 10 a) "," 0) 0)) "J") 1 0) 0))
(assert (str.contains (str.substr (str.substr b 10 a) 0 (- (str.indexof (str.substr b 10 a) "," 0) 0)) "G"))
(assert (= 0 (ite (str.contains (str.substr (str.substr b 10 a) 0 (- (str.indexof (str.substr b 10 a) "," 0) 0)) "B") 1 0)))
(assert (not (str.contains (str.substr (str.substr b 10 a) (+ (str.indexof (str.substr b 10 a) "," 0) 1) (str.len (str.substr b 10 a))) ",")))
(assert (distinct (str.len (str.substr (str.substr b 10 a) (+ (str.indexof (str.substr b 10 a) "," 0) 1) (- (str.len (str.substr b 10 a)) (+ (str.indexof (str.substr b 10 a) "," 0) 1)))) 0))
(assert (str.contains (str.substr b 10 a) ","))
(assert (not (str.contains (str.substr b 0 a) "?")))
(assert (str.prefixof "mongodb://" b))
(assert (>= (- (str.len (str.substr b 10 a)) (+ (str.indexof (str.substr b 10 a) "," 0) 1)) 0))
(check-sat)
[780] %