1 2 3 4 5 6 7 8 9 10
% EXPECT: sat x : STRING; y : STRING; ASSERT x = CONCAT( "abcd", y ); ASSERT LENGTH( x ) >= 6; ASSERT LENGTH( y ) < 5; CHECKSAT;