Creating a tactic from an invalid tactic results in a SIGSEGV

[bakerk98]

Had a lot of trouble with memory faults from nullpointers and finally figured out that I was using tactics that exist in the Python bindings but not the Rust bindings, namely "qfbv-new-sls"...

#[test]
    fn test_rust_z3_tactics(){
	let tactic = "qfbv-new-sls";
	let config = Config::new();
	let ctx: Context = Context::new(&config);

	//try to create a tactic from qfbv-new-sls if it exists
	let tactic : Tactic = Tactic::new(&ctx, tactic);
    }

results in

process didn't exit successfully: bin_name-a855b6c22e6f17f2 test_rust_z3_tactics --nocapture (signal: 11, SIGSEGV: invalid memory reference)

when we might expect to see an issue printed back to the user or something instead of this kind of failure. i think a check in z3_sys when we are making the new tactic to see if it returns a nullpointer back could help but I'm new to Rust so I'm not positive what the best fix might be

[Pat-Lafon]

If you want a drive-by suggestion, I would start at

z3.rs/z3/src/tactic.rs

Line 87 in 4f9fcfe

unsafe { Self::wrap(ctx, Z3_mk_tactic(ctx.z3_ctx, tactic_name.as_ptr())) }

Hoist out the Z3_mk_tactic into it's own line and then check whether it is null. From there you can panic with a message or something like that.

z3.rs/z3/src/ast.rs

Lines 576 to 578 in 4f9fcfe

	if numeral_ptr.is_null() {
	return None;
	}