[SMT-LIB] Multiarity XOR, IFF

Michal Moskal michal.moskal at gmail.com
Wed Nov 7 17:35:08 EST 2007


On 11/7/07, Cesare Tinelli <tinelli at cs.uiowa.edu> wrote:
> The standard *does* allow a multiarity = (with arity starting at 2).
> See, e.g., pages 36 and 37 of the standard.
> The semantics of (= a b c) is meant to be (and (= a b) (= b c)), as
> one would expect.

I find it strange, that (= a b c) is different from (iff a b c).

-- 
   Michał



More information about the SMT-LIB mailing list