Z3 / SMTLIB2 support for `distinct`

Question

I've been using the (ML) z3 bindings for a while, and the API function

val mk_distinct : context -> ast array -> ast

has served faithfully for many years. Am now trying to switch to the SMTLIB2 interface, but I find that the distinct command is unsupported. For example, the query:

(declare-fun x () Int)
(declare-fun y () Int)
(distinct x y)
(assert (= x y))
(check-sat)

yields the response:

unsupported
; distinct  
sat

on the web-demo. Is there some workaround?

Thanks!

Ranjit.

Answer 1

You should use (assert (distinct x y)) instead of (distinct x y). Here is a link to the updated example: http://rise4fun.com/Z3/uVrX