Wrong model given for formula on datatypes

[jad-hamza]

(declare-datatypes () ((X A B)))

(declare-const x X)

(assert (not (is-A x))) 
(assert (not (is-B x)))

(check-sat)
(get-model)

This should be unsat but succeeds with:

sat
(model 
  (define-fun x () X
    B)
)

[NikolajBjorner]

We are moving to SMT-LIB2.6 versions of recognizers. For now, try the following:

 (declare-datatypes () ((X A B)))
 (declare-const x X)
 (assert (not ((_ is A) x))) 
 (assert (not ((_ is B) x)))
(check-sat)

[jad-hamza]

Thanks!