Some questions about incremental SAT in Z3: can it be deactivated? Which techniques are used inside?

I am still in the process of learning the guts of Z3 (Python).

It was brought to my attention that Z3 performs incremental SAT solving by default (see SAT queries are slowing down in Z3-Python: what about incremental SAT?): specifically, every time you use the s.add command (where s is a solver), it means that it adds that clause to s, but it does not forget everything you have learned before.

First question: can non-incremental SAT solving be done in Z3? That is, somehow 'deactivate' the incremental solving. What would this mean? That we are creating a new solver for each enlarged formula?

For instance, this approach would be Z3-default-incremental:

...
  phi = a_formula
  s = Solver()
  s.add(phi)
  while  s.check() == sat: 
    s.check()
    m = s.model()
    phi = add_modelNegation(m)
    s.add(phi) #in order not to explore the same model again
  ...

That is, once we get a model, we attach the negated model to the same solver.

While this one is 'forcing' Z3 to be non-incremental:

...
  phi_st = a_formula
  s = Solver()
  s.add(phi_st)
  negatedModelsStack = []
  while  s.check() == sat:
    m = s.model()
    phi_n = add_modelNegation(m)
    negatedModelsStack.append(phi_n)
    original_plus_negated = And(phi_st, And(negatedModelsStack))
    s = Solver()
    s.add(original_plus_negated) #in order not to explore the same model again
  ...

That is, once we get a model, we attach the obtained models to a new solver.

Am I right?

On the other hand, in the attached link, the following is stated:

Compare this to, for instance, CVC4; which is by default not incremental. If you want to use CVC4 in incremental mode, you have to pass a specific command line argument

Does this mean in CVC4 you must create a new solver every time? Like in the second code?

Second question: how can I know exactly what techniques I am using to do incremental solving in Z3? I have been reading about incremental SAT theory and I see that one of those techniques is 'CDCL' (http://www.cril.univ-artois.fr/~audemard/slidesMontpellier2014.pdf), is this used in Z3's incremental search?

References: In order not to inundate Stack with similar questions, which readings do you recommend for incremental SAT in general and Z3's incremental SAT in particular? Also, is the incremental SAT of Z3 similar to the ones of other solvers such as MiniSAT or PySAT?

I'm not sure why you're trying to get z3 to act in a non-incremental way. But, if that's your goal, simply do not call check more than once: That's equivalent to being non-incremental. (Think of being incremental an "additional feature." You don't have to use it. The only difference between z3 and cvc4 is that the latter requires you to tell it ahead of time that you intend to use it in an incremental fashion, while the former is incremental by default.) As an end user you don't really need to know or care about the difference.

Side note If you start cvc4 without telling it to be incremental and call check twice, it'll complain. z3 won't. But otherwise the experience should be the same.

I don't think knowing how solvers implement incrementally is really helpful from a programming perspective. (It's of course paramount if you are implementing your own SMT solver.) There are many papers online for many aspects of SMT, though if you want to study the topic from scratch I recommend Daniel and Ofer's book on decision procedures: http://www.decision-procedures.org