Basile Clément

I think maintaining a separate list of declared symbols (as `Symbols.t`, not `Expr.t`) and inspecting that list at model generation time as I described above would also work without impacting...

The code in the issue now prints the following (with `--produce-models`): ``` unknown ( (define-fun a () Int 1) (define-fun b () Int 0) (define-fun c () Int (as @a0...

The `ac` modifier does not exist in the SMT-LIB language, and there is no support for modifiers on function declarations. I think that the most natural way (for users) to...

Postponing after discussion with the Why3 team, not a priority for now.

I tried to make a proper warning for this but it seems like it is blocked on Gbury/dolmen#218 — we don't have a clean way of of pre-empting the message...

IIRC the problem before #584 was not that Dolmen did not work for Windows but that the version we used was not available on the Windows OPAM repository ( https://github.com/ocaml-opam/opam-repository-mingw...

Additional note: interested users clarified that they wanted *native* Windows support, not Cygwin. AFAIK that means either waiting for OPAM 2.2 or using Diskuv. I'd say we wait for OPAM...

> From the inside however, we can do some ugly stuff. Instead of throwing the model away, is to try anyway to produce a model and cleanly catch any exception....

Although actually I am not sure this would be very smart, because #798 intend to introduce (backtrackable) mutable state in the theory as well :upside_down_face: What we *can* definitely do...

> > silently return an incorrect model (or, worse, to incorrectly report unsat > > It would not return silently an incorrect model, as the unknown reason would still be...