[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?