test/regress/regress0/datatypes/canExp-dtPendingMerge.smt2

   1 ; COMMAND-LINE: --ee-mode=distributed
   2 ; COMMAND-LINE: --ee-mode=central
   3 ; EXPECT: unsat
   4 (set-logic ALL)
   5 (set-info :status unsat)
   6 (declare-datatypes ((T 0)) (((A) (B (proj0B T) (proj1B T)) (C (proj0C T)) (D (proj0D T) ))))
   7 (declare-fun w () T)
   8 (declare-fun u () T)
   9 (assert (= w (B (D u) (B (D u) (C w)))))
  10 (check-sat)