fresh_const (and friends) are broken

[badboy]

Currently the semver test fails due to a version mismatch in the result.

I rewrote the test using ctx.numbered_int_const instead of ctx.fresh_int_const and it now passes (changes in https://gist.github.com/badboy/e126802b474d7de60d5d73e47531b01c/revisions)

I had a similar problem in my own code and also used numbered_int_const there.

[badboy]

Simplified failing test:

#[test]
fn test_fresh_int_const() {
    let _ = env_logger::try_init();
    let cfg = Config::new();
    let ctx = Context::new(&cfg);
    let x = ctx.fresh_int_const("x");
    let zero = ctx.from_i64(0);
    let solver = Solver::new(&ctx);
    solver.assert(&x.gt(&zero));
    assert!(solver.check());

    let model = solver.get_model();
    let xv = model.eval(&x).unwrap().as_i64().unwrap();
    assert_eq!(xv, 1);
}

Output:

thread 'test_fresh_int_const' panicked at 'assertion failed: `(left == right)`
  left: `0`,
 right: `1`', z3/tests/lib.rs:106:5

[badboy]

This C code example has the same problem.

[badboy]

As can be seen in this example the fresh const is not even part of the model, so I guess that's not how fresh_const should be used anymore?

Output from the example:

% ./z3-example 
result: 1
Model:
k!2 -> 1
y -> 1

[waywardmonkeys]

I'll try to look at this some today as well! Thanks!

[waywardmonkeys]

It is interesting to look at Z3_solver_to_string output from your C example:

(declare-fun k!1 () Bool)
(declare-fun x!0 () Int)
(declare-fun k!2 () Bool)
(declare-fun y () Int)
(declare-fun k!3 () Bool)
(declare-fun k!2 () Int)
(declare-fun k!4 () Bool)
(declare-fun k!5 () Bool)
(declare-fun k!6 () Bool)
(assert (> x!0 0))
(assert (> y 0))
(assert (> k!2 0))
(model-del k!1)
(model-add x!0 () Int (ite k!1 0 (+ 0 1)))
(model-del k!2)
(model-add y () Int (ite k!2 0 (+ 0 1)))
(model-del k!3)
(model-add k!2 () Int (ite k!3 0 (+ 0 1)))
(model-del k!4)
(model-add k!1 () Bool (not k!4))
(model-del k!5)
(model-add k!2 () Bool (not k!5))
(model-del k!6)
(model-add k!3 () Bool (not k!6))
(pb2bv-model-converter)
(model-add k!4 () Bool true)
(model-add k!5 () Bool true)
(model-add k!6 () Bool true)

[waywardmonkeys]

@jrakow and @cdisselkoen : Do either of you have any idea about this?

[djrenren]

This is also fixed on master. Somewhere in the AST refactoring it probably got fixed.

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

[djrenren]

Filed an issue with the z3 folks: Z3Prover/z3#2489

[djrenren]

As per the Z3 issue above, the problem has been confirmed to be a Z3 bug, and has been fixed on master. This is definitively not a bug in the bindings but in Z3 itself so I think we should close this issue.

[badboy]

Sounds good to me. Thanks for looking into that!