test/regress/regress1/bags/product3.smt2

   1 (set-logic ALL)
   2
   3 (set-info :status sat)
   4
   5 (declare-fun A () (Bag (Tuple Int Int Int)))
   6 (declare-fun B () (Bag (Tuple Int Int Int)))
   7 (declare-fun C () (Bag (Tuple Int Int Int Int Int Int)))
   8
   9 (assert (= C (table.product A B)))
  10
  11 (declare-fun x () (Tuple Int Int Int))
  12 (declare-fun y () (Tuple Int Int Int))
  13 (declare-fun z () (Tuple Int Int Int Int Int Int))
  14
  15 (assert (bag.member x A))
  16 (assert (bag.member y B))
  17 (assert (bag.member z C))
  18
  19 (assert (distinct x y ((_ tuple_project 0 1 2) z) ((_ tuple_project 3 4 5) z)))
  20
  21 (check-sat)