z3str-translator is a special build of CVC4 that merely parses and prints.
The SMT-LIBv2 printer of CVC4 is modified to support Z3-str string inputs.

The source code is available (for now) as a fork of cvc4, here:

  https://github.com/mdeters/cvc4/tree/z3str-translator

although this translation feature may be rolled into mainline CVC4
in future, in which case the above link will suffer from linkrot.

The "Kaluza" directory contains Kaluza benchmarks (in Kaluza/original),
their SMT-LIBv2 translations (in Kaluza/SMTLIB), and then the SMT-LIB
versions further translated into Z3-str inputs (in Kaluza/Z3STR).

Note that one benchmark failed during translation; in particular,
most Kaluza benchmarks that used regexes in a trivial way (such that
only a single string was in the language) were rewritten to equality
over strings in the Z3-str format.  One case:
  Kaluza/SMTLIB/sat/small/search.readable.smt2 uses regexes i
was a bit (though not much) more complicated, and was translated by hand.

-- Morgan Deters <mdeters@cs.nyu.edu> Thu, 06 Feb 2014 15:48:19 -0500