`zz` leaves zombie process of `z3`

[dm9pZCAq]

---

during building zz leaves zombie processes of z3

i found that processes spawns here: https://github.com/zetzit/zz/blob/18020b10b933cfe2fc7f2256b71e646889f9b1d2/src/smt.rs#L1005

and from rsmt2 sources i found that process should be automatically waited at kill and kill happens at Solver drop
https://docs.rs/rsmt2/0.14.0/src/rsmt2/solver.rs.html#266-300 https://docs.rs/rsmt2/0.14.0/src/rsmt2/solver.rs.html#75-80

i think the problem is solver not dropping at time, but zz/src/stm.rs is too complicated for me to found it myself

[aep]

hm lifetime of the solver is supposed to be contained within symbolic::execute

https://github.com/zetzit/zz/blob/b797fe995876b6e0b83aa415aefbb062f8b2ed65/src/symbolic.rs#L5038

if there's an extra step needed, it should be done somewhere in that function

[dm9pZCAq]

hmm this MRE leaves zombie after drop, so problem is in rsmt2

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(())
}

[aep]

does this occur before #162 as well? they might have introduced a bug recently

[dm9pZCAq]

yes, it was before

[aep]

hmm i've never seen that. maybe its a new bug in z3. can you try with yices2?

[dm9pZCAq]

no, i think this is bug in rsmt2

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

i will open issue about this on rsmt2 repo

[AdrienChampion]

FYI: this issue was (just) fixed in rsmt2 v0.14.1.