Assume that I have asserted some formula P and, after checking satisfiability, obtained from Z3 a partial model for it, let's call it M.
Now, would it be possible to test whether another formula Q can be satisfied by extending, if necessary, the current model M. That is, I want to check whether the formula P and Q is satisfiable but fixing the values that have been assigned by the current partial model.
Alternatively, is it possible to ask Z3 to “complete” a specific partial model? (That is, I still want to obtain partial models; but, in a few cases, I would like to be able to extend a partial model so that I can then evaluate some arbitrary formula Q which might contain constants/functions not assigned by the current model)