Model for abstract functions about inox HOT 8 CLOSED

Inox will assume (define-fun ...) to define some interpreted function so it'll ignore it when reporting models. You can use (define-const ...) and then rely on the constant in your assertions (I seem to have a bug with global variables that aren't referred to in assertions for now, I'll ping this issue once it's fixed).

from inox.

I meant displaying the value of undefined constants such as (declare-fun foo () bar)

from inox.

Ah yes I meant replace (declare-fun ...) by (declare-const ...), sorry.

from inox.

Hmm, is declare-const valid TIP?

edit: nevermind, indeed it is.

from inox.

Well it's in the BNF at https://tip-org.github.io/bnf.html

from inox.

Indeed, I even parse it. The only issue in my specific case is that most of my constants are introduced in the goal, as in (assert-not (forall ((x a) (y b)) …), but that's ok I guess.

from inox.

I'm going to hijack this issue to remember to output models for abstract functions (declare-fun) at some point.

from inox.

Fixed in 51a3a34

from inox.