Incorrect s-expression: the reserved word 'exists' is currently not interpreted in s-expressions

[jhjourdan]

On the following smt2 file:

bug_altergo.psmt2.txt

Alt-ergo 2.6.2 fails with error message:

Error Incorrect s-expression: the reserved word 'exists' is currently not interpreted in s-expressions,
      please report upstream if you think it should be interpreted

The problem is that a quantifier is used in a trigger, which I thing should be accepted, even if completely ignored by the prover.

[bclement-ocp]

Thanks for the report. We (or rather, dolmen which we use for parsing SMT-LIB input) follow the SMT-LIB specification here -- the terms provided in :pattern expressions are supposed to be binder-free (see section 3.6.5, Term attributes).

Can you provide more context on why you need to include quantifiers in patterns? We can consider supporting this (by ignoring it) in the psmt2 format, but this is also rejected by Z3 — with a better error message than ours, "patterns cannot be variables or quantifiers" — so presumably Why3 would need a way to deal with this anyway.

[jhjourdan]

When you specify a trigger in a generic context, it may be an opaque symbol which makes a lot of sense as a trigger. However, at some point, this symbol may get defined as an arbitrary term (which may include a binder), and Why3 transforms may unfold it.

That being said, if the SMT-LIB spec says this is forbidden, it may be the role of Why3 to remove such a trigger...

[jhjourdan]

We can consider supporting this (by ignoring it) in the psmt2 format, but this is also rejected by Z3

At least with z3 4.12.4, my tests indicate that this is accepted by Z3.

[jhjourdan]

We can consider supporting this (by ignoring it) in the psmt2 format, but this is also rejected by Z3

At least with z3 4.12.4, my tests indicate that this is accepted by Z3.

See attachment for this : z3.smt2.txt

This is actually more subtle: Z3 emits an error message, but is still able to process the file and answer unsat....

[bclement-ocp]

When you specify a trigger in a generic context, it may be an opaque symbol which makes a lot of sense as a trigger. However, at > some point, this symbol may get defined as an arbitrary term (which may include a binder), and Why3 transforms may unfold it.

I see, that makes sense — thanks. I still think Why3 should be the place to deal with this — I would say that ideally Why3 should not unfold definitions inside of triggers, but I understand something needs to be done if the original symbol is removed from the problem.

This is actually more subtle: Z3 emits an error message, but is still able to process the file and answer unsat....

Z3 by default ignores invalid statements (after printing an error message) and continues with the rest of the input. Alt-Ergo on the other hand stops as soon as it encounters an error.

As far as I can tell, Z3 should be ignoring not only the pattern but the whole quantifier; see for instance the following input file where Z3 emits an error message then replies sat.

(set-logic ALL)
(get-info :error-behavior)

(declare-fun P (Int Int) Bool)

(assert (forall ((x Int)) (! (= x 0) :pattern ((exists ((y Int)) (P x y))))))

(check-sat)

If you set the error-behavior to immediate-exit using (set-option :error-behavior immediate-exit), Z3 also stops at the error.