Can the Z3 run in incremental mode?

Question

I use Z3 in QFBV formulas. I was wondering if Z3 can work on formulas like SAT solvers can on boolean clauses step by step. 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 the Z3 support recognizable information? Can i use z3 gradually?

Thank.

Answer 1

Yes, Z3 can do this if you use assumptions. This is discussed here: Soft / hard restrictions in Z3