Может ли Z3 работать в инкрементном режиме?

Я использую Z3 в формулах QFBV. Мне было интересно, может ли Z3 работать постепенно с такими формулами, как решатели SAT, могут работать с логическими предложениями. В основном мне нужен способ реализовать следующий цикл:

F = initial QFBV formula
while(F is unsat) {
    F := F Union {some additional QFBV formula based on unsat core}
}

Поддерживает ли Z3 изученную информацию? Могу ли я использовать z3 постепенно?

Спасибо.