OSTRICH Web Interface

OSTRICH is an SMT solver for string constraints.
Constraints for OSTRICH can be written using a superset of a subset of the new SMT-LIB string theory. For more details, see the OSTRICH github page.

Load a predefined example: concat regex-parsing replace-1 replaceall-1 replaceall-2 replaceall-regex-1 successor-OSTRICH successor-seq to-uppercase tree-of-strings adts1 bv-equation bv-interpolation1 bv-interpolation2 bv-interpolation3 bv-interpolation4 interpolation1 modulo palindrome quantifiers1 quantifiers2 template bv-interpolation-1 bv-interpolation-2 bv-interpolation-3 datatype1 datatype2 datatype3 incremental interpolation1 quantifier-elimination-2 quantifier-elimination simple GEG021=1 ex:1 ex:10 ex:2 ex:3 ex:5 ex:6 ex:7a ex:7b ex:8 ex:P1 ex:P2 ... or enter some formulas: