StringFuzz is a problem instance generator and fuzzer for SMT string solvers like CVC, Z3, and norn. It is useful for string solver developers and testers, and can help expose bugs and performance issues. See installation instructions here.

Strings

Make an UNSAT string instance:

> stringfuzzg overlaps --num-vars 1 --length-of-consts 10

(set-logic QF_S)
(declare-fun var0 () String)
(assert (= (str.++ "NR5x$!PCZJ" var0) (str.++ var0 "-r#hAhc<w'")))
(check-sat)

solve it with CVC4:

> stringfuzzg overlaps --num-vars 1 --length-of-consts 10 | cvc4 --lang smt
unsat

Regexes

Make a SAT regex instance:

> stringfuzzg -m regex --literal-type increasing --depth 2 --num-terms 2

(set-logic QF_S)
(declare-fun var0 () String)
(assert (str.in.re var0 (re.++ (re.+ (re.+ (str.to.re "00"))) (re.union (re.+ (str.to.re "11")) (re.+ (str.to.re "22"))))))
(check-sat)
(get-model)

solve it with Z3:

> stringfuzzg -m regex --literal-type increasing --depth 2 --num-terms 2 | z3str3 smt.string_solver=z3str3 -in
sat
(model
  (define-fun var0 () String
    "00000000000000000000000000000000001111")
)

Try It

Explore further by looking at the other generators:

> stringfuzzg --help

and transformers:

> stringfuzzx --help