z3-sys: Fix return type of Z3_parse_smtlib2_string and Z3_parse_smtlib2_file

prove-rs / z3.rs

Rust bindings for the Z3 solver.

338 stars 105 forks source link

Closed dp1 closed 1 year ago

dp1 commented 1 year ago

Z3_parse_smtlib2_string and Z3_parse_smtlib2_file are marked as returning a Z3_ast, while they should be returning a Z3_ast_vector (https://z3prover.github.io/api/html/group__capi.html#ga7905ebec9289b9fe5debcad965f6267e). This (tiny) PR fixes the problem.

dp1 commented 1 year ago

Just a ping for this - in its current state it causes a nasty type confusion when using the bindings, leading to crashes later in the execution.

waywardmonkeys commented 1 year ago

Ah, this happened in Z3 4.8.

Thanks!