child processes not properly waited and leaves zombie processes

[dm9pZCAq]

---

here is MRE

use rsmt2::parse::{
    IdentParser,
    ModelParser,
};
use rsmt2::{
    SmtRes,
    Solver,
};
use std::io;
use std::io::prelude::*;

type BoxedErr = Box<dyn (::std::error::Error)>;
type Result<T> = ::std::result::Result<T, BoxedErr>;

#[derive(Clone, Copy)]
struct Parser;

impl<'a> IdentParser<String, String, &'a str> for Parser {
    fn parse_ident(self, input: &'a str) -> SmtRes<String> {
        Ok(input.into())
    }
    fn parse_type(self, input: &'a str) -> SmtRes<String> {
        Ok(input.into())
    }
}

impl<'a> ModelParser<String, String, String, &'a str> for Parser {
    fn parse_value(
        self,
        input: &'a str,
        _ident: &String,
        _params: &[(String, String)],
        _typ: &String,
    ) -> SmtRes<String> {
        Ok(input.into())
    }
}

fn main() -> Result<()> {
    let mut solver = Solver::default_z3(Parser)?;

    solver.define_fun("sq", &[("n", "Int")], "Int", "(* n n)")?;
    solver.declare_const("n", "Int")?;
    solver.declare_const("m", "Int")?;

    solver.assert("(= (+ (sq n) (sq m)) 29)")?;
    solver.assert("(and (< n 5) (> n 0) (> m 0))")?;

    let is_sat = solver.check_sat()?;
    assert!(is_sat);
    let mut model = solver.get_model()?;

    drop(solver); // force drop

    model.sort();
    println!("{:?}", model);

    io::stdin().read(&mut [0u8])?; // pause

    Ok(())
}

htop shows that there is zombie process of z3

---

here is process not properly waited https://github.com/kino-mc/rsmt2/blob/03236219276bebf9b5be4bf6974d781f155c1f0f/src/solver.rs#L279-L300

and here is brief explanation about zombies https://doc.rust-lang.org/stable/std/process/struct.Child.html#warning

---

(related issue https://github.com/zetzit/zz/issues/163)

[AdrienChampion]

Thank you!

That's concerning, I'll take a close look shortly.

[AdrienChampion]

Right, so, I opened a PR to fix this problem. Thank you again for this issue, and in particular for the MRE. It made my life significantly easier 😸

I don't like the idea of block-wait-ing too much, I'm afraid it might freeze user code when/if there is a problem somewhere. So I ended up try_wait-ing at 10ms intervals until either the child process is done (nominal case), or 1s has elapsed which raises an error.

This does the job on my machine (Apple M1) on your MRE, can you confirm it solves the problem on your end too?

[dm9pZCAq]

yes, it solves the problem for me too

thank you