Missformed SMT source, Unknown SMT term of class: class smtlib.trees.Terms$FunctionApplication

[vkuncak]

The snack dispenser example, https://github.com/epfl-lara/bolts/blob/main/tutorials/dispenser/Dispenser.scala fails with smt-cvc5 with error messages apparently during Inox's preparation of the SMT-LIB file.

(Note: the benchmark only works with a substantial timeout with 43 seconds on my laptop to check exampleTrace postcondition; something that was likely not happening before.)

[sankalpgambhir]

The error is apparently not in the generation of the SMT2 file, but rather in reading the SMTLIB model into Inox terms (In Inox: SMTLIBParser.scala:226). It starts here while reading function definitions from the model.

This seems to be caused by the fact that cvc5 is outputting a model where the model for one function uses the generated model for another function (but is returning them in the opposite order). Illustrated here:

Definitions:

(declare-fun lt () State)
(declare-fun r (State Action) Option)

And the model:

(define-fun lt () State (valueOf (r [...]) ; trimmed
(define-fun r ((arg1 State) (arg2 Action)) Option None)

(cleaned up a bit for readability)

There is also a valueOf None expression, which as far as I can tell, is assigned some unique value while testing for satisfiability (and is not returned).

Inox doesn't seem to expect this usage of functions and thus returns it as an unknown symbol. I'm checking if this is unexpected behaviour from the solver, or a failure to read it from Inox's end because of the order they are returned in.

z3 does not have this behaviour on this example, at least. Its model does not use other functions at all, only lets and ADT constructors.

[vkuncak]

I suspected this and tried to use --check-models=false but that turns off only our execution base validation. Can we make it turn off reconstruction of the model as well, so it only gets a boolean answer?

On Fri, 2 Aug 2024, 08:46 Sankalp Gambhir, @.***> wrote:

The error is apparently not in the generation of the SMT2 file, but rather in reading the SMTLIB model into Inox terms (In Inox: SMTLIBParser.scala:226 https://github.com/epfl-lara/inox/blob/3f5bd759182f1c07ac1da2c48ed75c759bfe95ba/src/main/scala/inox/solvers/smtlib/SMTLIBParser.scala#L226). It starts here while reading function definitions from the model https://github.com/epfl-lara/inox/blob/3f5bd759182f1c07ac1da2c48ed75c759bfe95ba/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala#L81 .

This seems to be caused by the fact that cvc5 is outputting a model where the model for one function uses the generated model for another function. Illustrated here:

Definitions:

(declare-fun lt () State) (declare-fun r (State Action) Option)

And the model:

(define-fun lt () State (valueOf (r [...]) ; trimmed (define-fun r ((arg1 State) (arg2 Action)) Option None)

(cleanup up a bit for readability)

There is also a valueOf None expression, which as far as I can tell, is assigned some unique value while testing for satisfiability (and is not returned).

Inox doesn't seem to expect this usage of functions within each other. I'm checking if this is expected behaviour from the solver, or a failure to read it from Inox's end. z3 does not have this behaviour on this example, at least.

— Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/1549#issuecomment-2264679448, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA5CDN23IKKNGJZQAJRC4XTZPMTLTAVCNFSM6AAAAABLZF7N7WVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENRUGY3TSNBUHA . You are receiving this because you authored the thread.Message ID: @.***>

[sankalpgambhir]

That's correct, the "check model" option is only checked after retrieval and construction of the model in the unrolling solver.

The requirement of a model is encoded in the types and API as well (ResponseWithModel[Model { val program: self.program.type }]). We can widen this in the SimpleSolver API to just CheckResponse but I have to see if the removal of the refinement on program changes anything. (Likely safe)

After that it's a matter of changing the one-line check call itself to not ask for a model if the option is not requested. If the check call does not ask for a model, the corresponding call for model reconstruction does not happen, from what I can see; (get-model) is not even emitted to the solver.

[sankalpgambhir]

Would you prefer to make this part of the --check-models option or a new option? (In any case, I will investigate the original issue as well; it should not fail on the default settings this way)

[sankalpgambhir]

Regarding the original issue: the order of definitions returned is not an issue, that is accounted for. Inox does also allow seeing some (marked) constants reused, but it never expects actual functions with parameters. The function r here is neither marked nor a constant (per its type).

[samuelchassot]

I also wanted to remove model reconstruction when using --simple-models option, as Inox does not expect a model that does not assign all variables (if I remember correctly). I think that adds to the pool of justifications to do it.

[sankalpgambhir]

With ignore-models, this can be successfully verified now on the PR linked above. However, the issue of supporting models from cvc5 still stands.

Can I move this issue to Inox instead?

[vkuncak]

You can move the issue as desired.