Constant evaluates to false when calling Model::eval

[aochagavia]

I have an issue where a constant is evaluated to false when calling Model::eval, even though the solver says that the constant is true in the model.

Code

use z3::{Ast, Config, Context, Solver};

fn main() {
    let config = Config::new();
    let context = Context::new(&config);
    let solver = Solver::new(&context);

    let b = context.fresh_bool_const("b");
    let true_ = Ast::from_bool(&context, true);
    let expr = Ast::_eq(&b, &true_);
    solver.assert(&expr);
    assert!(solver.check());

    println!("Solver: {}", solver.to_string());

    let model = solver.get_model();
    println!("b = {}", model.eval(&b).unwrap().as_bool().unwrap());
}

Expected behavior

After calling solver.check, solver.to_string returns:

(declare-fun b!0 () Bool)
(assert (= b!0 true))
(rmodel->model-converter-wrapper
b!0 -> true
)

I have no prior experience with Z3, but I read this as: a solution was found where b!0 is true. Therefore, I expect model.eval(&b).unwrap().as_bool().unwrap() to be true

Actual behavior

model.eval(&b).unwrap().as_bool().unwrap() returns false

[heinzelotto]

I'm not sure why but it works if you use the named_const functions, e. g. named_bool_const instead of fresh_bool_const.

[cdisselkoen]

#2 is related.

[waywardmonkeys]

I'd really like to see this sorted out before I make a new release. Any volunteers?

[djrenren]

So... this appears to be working on master. I'd close this as fixed unless anyone can still repro

#[test]
fn testing() {
    let config = Config::new();
    let context = Context::new(&config);
    let solver = Solver::new(&context);

    let b = ast::Bool::fresh_const(&context, "b");
    let true_ = ast::Bool::from_bool(&context, true);
    let expr = Ast::_eq(&b, &true_);
    solver.assert(&expr);
    assert!(solver.check() == SatResult::Sat);

    println!("Solver: {}", solver.to_string());

    let model = solver.get_model();
    let b = model.eval(&b).unwrap().as_bool().unwrap();
    println!("b = {}", b);
    assert!(b);
}

[djrenren]

Nevermind! Updated my z3 from 4.5 to 4.8 and now it's broken again. Seems like something changed in the API. I'll do some digging.

[cdisselkoen]

I can repro: the test in the above comment fails on current master on my machine when using Z3 4.8.5.

[djrenren]

See Z3 issue: Z3Prover/z3#2489 (fixed in: Z3Prover/z3@fcc7bd3)

@waywardmonkeys: This is a Z3 bug, that is now fixed in master and affects versions 4.8.1 - 4.8.5, so I don't think it should be a blocker for releasing an update.

[waywardmonkeys]

@djrenren Thanks for taking this up!

[waywardmonkeys]

z3 4.8.6 is out now and this is fixed.