Генерация данных для запуска всех возможных путей в программе

Я новичок в Z3 и искал ответ на мой вопрос здесь и в Google. Я не был успешным.

Это код, вызывающий проблему:

void test(string str) {
if (str [0] == 'g') {
cout << "\"The first letter g" case"<< endl;
if (str [1] == 'a') cout << "Second letter is 'a'";
else cout << "Second letter is not 'a'";
} else {
cout << "The non-g case" << endl;
if (str [1] == 'b') cout << "Second letter is 'b'";
else cout << "Second letter is not 'b'";
}
}

Мне нужно автоматически сгенерировать входные данные, чтобы код выполнялся полностью.
Можно ли вообще сделать это с z3? Если да, то как я могу это сделать с помощью API z3 C / C ++?