Set the default error handler to None

[SeeSpring]

In other language bindings, after constructing the context the error handler is set to null/a noop. This should fix #69 .

In the C++ bindings, null is passed.
https://github.com/Z3Prover/z3/blob/141edef0d64796fd387ec2f8efe796a7329c48e2/src/api/c%2B%2B/z3%2B%2B.h#L167
In the ML, Python, and C# bindings, a pointer to a noop function are
passed instead, to the same effect.
https://github.com/Z3Prover/z3/blob/141edef0d64796fd387ec2f8efe796a7329c48e2/src/api/ml/z3native_stubs.c.pre#L448
https://github.com/Z3Prover/z3/blob/141edef0d64796fd387ec2f8efe796a7329c48e2/src/api/python/z3/z3.py#L187
https://github.com/Z3Prover/z3/blob/141edef0d64796fd387ec2f8efe796a7329c48e2/src/api/dotnet/Context.cs#L4627

[fitzgen]

Can you describe what happens now when get_model is called on a solver that doesn't have a satisfiable answer? Does it hang? Does it return an empty model?

[SeeSpring]

get_model should return a null pointer if the solver is unsatisfiable. I think another option would be to change get_model to return Option<Model<'ctx>> and have Z3_model be a nonnull pointer.

[fitzgen]

get_model should return a null pointer if the solver is unsatisfiable

So would that lead to UB with the current patch, which always returns a Model?

I think another option would be to change get_model to return Option<Model<'ctx>> and have Z3_model be a nonnull pointer.

Yes, I think this would be preferable.

[SeeSpring]

One issue is that Z3_model is defined in z3-sys as

pub type Z3_model = *mut _Z3_model;

so don't think it can be made into non-null without changing bindgen. Another option would be to panic if Z3_ast_map_find/Z3_optimize_get_model/Z3_params_validate/Z3_solver_get_model/Z3_solver_get_proof would have normally invoked the error handler. C++ calls and checks Z3_get_error_code but Java, C# and ML only check if the return value is null.

[fitzgen]

We wouldn't change the z3-sys bindings, just the higher-level z3 crate built on top of them.

[SeeSpring]

One issue with this is that this would be semver breaking since it changes function signatures vs panicking if we get null.

[fitzgen]

Releasing a new breaking version isn't a big deal.

[fitzgen]

Thanks!