Can Z3 work in incremental mode?

Question

I am using Z3 on QFBV formulas . I was wondering if Z3 can work incrementally on such formulas like SAT solvers can on boolean clauses. Basically I need a way to implement the following loop:

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

Does Z3 maintain the learned information? Can I use z3 incrementally?

Thanks.

Answer 1

Yes, Z3 can do that if you use assumptions. This is discussed here: Soft/Hard constraints in Z3