[Help Wanted] Why incremental mode does not keep num of decisions down in this case?

[aur3l14no]

I have this following case modified from tests/lib.rs

fn test_pb() {
    let cfg = Config::new();
    let ctx = Context::new(&cfg);
    let x = ast::Bool::new_const(&ctx, "x");
    let y = ast::Bool::new_const(&ctx, "y");

    let a = ast::Bool::new_const(&ctx, "a");
    let b = ast::Bool::new_const(&ctx, "b");
    let c = ast::Bool::new_const(&ctx, "c");
    let d = ast::Bool::new_const(&ctx, "d");
    let solver = Solver::new(&ctx);
    solver.push();

    // this line
    solver.assert(&ast::Bool::pb_eq(
        &ctx,
        &[(&a, 1), (&b, 1), (&c, 1), (&d, 1)],
        2,
    ));

    solver.push();
    solver.assert(&ast::Bool::pb_eq(&ctx, &[(&x, 1), (&y, 1)], 1));
    assert_eq!(solver.check(), SatResult::Sat);
    let model = solver.get_model().unwrap();
    let xv = model.eval(&x, true).unwrap().as_bool().unwrap();
    let yv = model.eval(&y, true).unwrap().as_bool().unwrap();
    info!("x: {}", xv);
    info!("y: {}", yv);
    assert!((xv && !yv) || (!xv && yv));
    info!("{:?}", solver.get_statistics());
    solver.pop(1);

    solver.push();
    solver.assert(&ast::Bool::pb_ge(&ctx, &[(&x, 1), (&y, 1)], 2));
    assert_eq!(solver.check(), SatResult::Sat);
    let model = solver.get_model().unwrap();
    let xv = model.eval(&x, true).unwrap().as_bool().unwrap();
    let yv = model.eval(&y, true).unwrap().as_bool().unwrap();
    info!("x: {}", xv);
    info!("y: {}", yv);
    assert!(xv && yv);
    info!("{:?}", solver.get_statistics());
    solver.pop(1);

    solver.assert(&ast::Bool::pb_le(&ctx, &[(&x, 1), (&y, 1)], 0));
    assert_eq!(solver.check(), SatResult::Sat);
    let model = solver.get_model().unwrap();
    let xv = model.eval(&x, true).unwrap().as_bool().unwrap();
    let yv = model.eval(&y, true).unwrap().as_bool().unwrap();
    info!("x: {}", xv);
    info!("y: {}", yv);
    assert!(!xv && !yv);
    info!("{:?}", solver.get_statistics());

    let res = solver.check();
    info!("{res:?}");

    info!("{:?}", solver.get_statistics());
}

Basically I want to see that the assertion (a+b+c+d==2) has only one-time affect on the number of decisions, since it is pushed to the bottom of the assertion stack and have no affect on other assertions.

However, without that assertion, the final number of decisions is 1 while with that assertion, the final number of decision becomes 11.

Is there something that I've missed?

[Pat-Lafon]

So I know that push/pop saves lemmas between calls, but it's not clear to me that it would save the values it chose between runs(which is what I think this is talking about? that once the solver chooses values for a,b,c,d you never need to choose them again).

Is there documentation about this that I could look at? Or is this an assumption about how the solver operates(maybe this query is simple enough that you can dig through the logs to see what Z3 does here?)?