FuncInterp::get_else should return an Option

[toolCHAINZ]

Noticed while investigating #459

    /// Returns the else value of the function interpretation.
    /// Returns None if the else value is not set by Z3.
    pub fn get_else(&self) -> Dynamic {
        unsafe {
            Dynamic::wrap(
                &self.ctx,
                Z3_func_interp_get_else(self.ctx.z3_ctx.0, self.z3_func_interp).unwrap(),
            )
        }
    }

This doc comment does not match the return type of this function. I believe the raw Dynamic is correct, as an else is always returned (as far as I can tell).

[Pat-Lafon]

Hmm, interesting. The documentation is taken from the python bindings it seems: https://z3prover.github.io/api/html/z3py_8py_source.html#l06308 But it's actually pretty hard to try to get this to return None? I think the only way is by providing a null pointer to set_else(but with the recent changes, the Z3_Ast is a NonNull in the z3_sys bindings).

[toolCHAINZ]

Looking through the upstream code it does seem that the else is optional (and func interps are allowed to be partial):

https://github.com/Z3Prover/z3/blob/11fb5c7dc49d879cdc2a3c3c4a732cd3c39749c5/src/model/func_interp.h#L121
https://github.com/Z3Prover/z3/blob/11fb5c7dc49d879cdc2a3c3c4a732cd3c39749c5/src/api/api_model.cpp#L322

I have not been able to make Z3 actually give me such a func interp, but clearly it's possible. I guess we should change this to Option<Dynamic> and change set_else and it's z3-sys counterpart to take in an Option<Dynamic>