Wrong model on elementary integer problem

[Halbaroth]

Alt-Ergo produces a wrong model for this problem:

(set-logic ALL)
(set-option :produce-models true)
(declare-const i Int)
(define-fun C ((i Int)) Bool (> i 0))
(assert (C i))
(check-sat)
(get-model)

outputs

unknown
(
  (define-fun i () Int 0)
)

But the slightly different input:

(set-logic ALL)
(set-option :produce-models true)
(declare-const i Int)
(assert (> i 0))
(check-sat)
(get-model)

produces a correct model:

unknown
(
  (define-fun i () Int 2)
)

I used the command dune exec -- alt-ergo --produce-model --frontend dolmen.

[bclement-ocp]

Ah interesting. Something weird is going on because we have i → 2 in the UF representative map before generating the model, but it looks like model generation happens in a fresh context somehow? Maybe this is related to #739?

[Halbaroth]

Yes, it is! We can see it if we use --dump-models instead of --produce-models. I will fix this bug for the release 2.5.0.