test/regress/regress0/strings/ncontrib-rewrites.smt2

   1 (set-logic ALL)
   2 (set-info :status unsat)
   3 (declare-fun x () String)
   4 (declare-fun y () String)
   5 (declare-fun z () String)
   6
   7 (assert (or
   8
   9 (not (= (str.replace (str.++ x x) "A" "B") (str.replace x "" (str.replace x "A" "B"))))
  10
  11 (not (= (str.replace (str.++ x y "B" x y) "A" z) (str.++ (str.replace (str.++ x y) "A" z) "B" x y)))
  12
  13 ))
  14
  15 (check-sat)