All problems in one archive can be found here:
problems.zip.
Name  Sample Instances  # of Instances  SAT/UNSAT  Description  
lengthsshort 
first.smt20
first.smt25 last.smt20 last.smt25 
50  sat  Each instance has 30 variables. Each variable’s length is constrained randomly from 0 to X.


lengthslong 
first.smt20
first.smt25 last.smt20 last.smt25 
50  sat  Each instance has 30 variables. Each variable’s length is constrained randomly from 0 to X.


lengthsconcats 
first.smt20
first.smt25 last.smt20 last.smt25 
50  sat  Each instance has X variables, and Y random unique binary concats of those variables.


concatssmall 
first.smt20
first.smt25 last.smt20 last.smt25 
50  sat  Each instance is a rightheavy concat tree of depth X,
equal to the string


concatsbig 
first.smt20
first.smt25 last.smt20 last.smt25 
30  sat  Each instance is a rightheavy concat tree of depth X,
equal to the string


concatsbalanced 
first.smt20
first.smt25 last.smt20 last.smt25 
10  sat  Each instance is a balanced concat tree of depth X,
equal to the string


concatsextractssmall 
first.smt20
first.smt25 last.smt20 last.smt25 
50  sat  Each instance is a rightheavy concat tree of depth 30,
equal to the string


concatsextractsbig 
first.smt20
first.smt25 last.smt20 last.smt25 
30  sat  Each instance is a rightheavy concat tree of depth 30,
equal to the string


overlapssmall 
first.smt20
first.smt25 last.smt20 last.smt25 
30  both  Each instance is an equation of the form a.V = V.b, where V is a concatenation of X variables.


overlapsbig 
first.smt20
first.smt25 last.smt20 last.smt25 
10  both  Each instance is an equation of the form a.V = V.b, where V is a concatenation of X variables.


regexsmall 
first.smt20
first.smt25 last.smt20 last.smt25 
30  sat  Each instance tests whether a variable belongs to a random regex. The regex is a concatenation of X random regex terms of depth 2.


regexbig 
first.smt20
first.smt25 last.smt20 last.smt25 
30  sat  Each instance tests whether a variable belongs to a random regex. The regex is a concatenation of X random regex terms of depth 2.


regexdeep 
first.smt20
first.smt25 last.smt20 last.smt25 
15  both  Each instance tests whether a variable belongs to a random regex. The regex is a concatenation of 2 random regex terms of depth X. The variable is at least 15 characters long.


manyregexes 
first.smt20
first.smt25 last.smt20 last.smt25 
20  both  Each instance tests whether a variable is in X regexes. Each regex is a concatenation of 10 terms of depth 2.


regexpair 
first.smt20
first.smt25 last.smt20 last.smt25 
20  both  Each instance tests whether a variable is in one regex but not another. Each regex is a concatenation of X terms of depth 2.


regexlengths 
first.smt20
first.smt25 last.smt20 last.smt25 
20  both  Each instance tests whether a variable is in a regex, and constrains the variable to a minimum length of X. The regex contains 10 terms, each of depth 2.
