SMT-LIB: quoted symbols ar treated as distinct symbols

[hansjoergschurr]

In SMT-LIB symbols can be quoted by enclosing them in |, e.g., |A|. According to the SMT-LIB standard (3.1 Symbols Page 23) a quoted and an unquoted symbol is the same symbol:

Following Common Lisp’s conventions,enclosing a simple symbol in vertical bars does not produce a new symbol. This means for instance that abc and |abc| are the same symbol.

Dolmen, however, does not follow this convention and the following SMT-LIB problem produces an error:

(set-logic QF_UF)
(declare-sort S 0)
(declare-const |A| S)
(declare-fun f (S) Bool)
(assert (not (f A)))
(check-sat)

[Gbury]

Good catch ! I'm working on a fix