Z3 will not case split on hand-crafted data types

Question

I have defined my own booleans, called boolean is SMT2, and the AND function boolean_and over them. My conjecture is that AND is commutative:

(declare-sort boolean)
(declare-const sk_x boolean)
(declare-const sk_y boolean)
(declare-const boolean_false boolean)
(declare-const boolean_true boolean)
(declare-fun boolean_and (boolean boolean) boolean)

;; axiomatize booleans: false /= true and every bool is true or false
(assert (forall ((x boolean)) (or (= x boolean_false)
                                  (= x boolean_true))))

(assert (not (= boolean_false boolean_true)))

;; definition of AND
(assert (forall ((a boolean)) (= (boolean_and boolean_false a) boolean_false)))
(assert (forall ((a boolean)) (= (boolean_and boolean_true a) a)))

;; try to prove that AND is commutative
(assert (not (= (boolean_and sk_x sk_y)
                (boolean_and sk_y sk_x))))

(check-sat)

However, z3 reports unknown on this problem after a while, even though I thought it should be able to use my case split assertions on the skolemised variables sk_x and sk_y.

Curiously, if I remove my boolean axiomatization and replace it with declare-datatypes, z3 will report unsat:

(declare-datatypes () ((boolean (boolean_true) (boolean_false))))

(declare-const sk_x boolean)
(declare-const sk_y boolean)
(declare-fun boolean_and (boolean boolean) boolean)

(assert (forall ((a boolean)) (= (boolean_and boolean_false a) boolean_false)))
(assert (forall ((a boolean)) (= (boolean_and boolean_true a) a)))

(assert (not (= (boolean_and sk_x sk_y)
                (boolean_and sk_y sk_x))))

(check-sat)

What am I doing wrong? How can I get z3 to case split using my axiomatization?

Answer 1

You are not doing anything wrong. The official release (v4.3.1) may fail on problems containing cardinality constraints such as

(assert (forall ((x boolean)) (or (= x boolean_false)
                                  (= x boolean_true))))

This constraint is asserting that the uninterpreted sort boolean has at most two elements. I fixed this problem. The fix is already available in the unstable branch. Here are some instructions on how to compile the unstable branch. Tomorrow, the nightly builds will also contain this fix.