test/regress/regress1/push-pop/cee-prs-small.smt2

   1 ; COMMAND-LINE: -i --ee-mode=distributed
   2 ; COMMAND-LINE: -i --ee-mode=central
   3 ; EXPECT: sat
   4 ; EXPECT: unsat
   5 (set-logic ALL)
   6 (declare-datatypes ((r 0)) (((r_ctor (x Int)))))
   7 (declare-datatype tup ((mkt (t1 (Array Int Int)) (t2 (Array Int Int)))))
   8 (declare-datatypes ((q 0)) (((R (x (Array Int r)) (y tup)))))
   9 (declare-fun z () q)
  10 (assert (not (= 1 (select (t2 (y z)) 1))))
  11 (assert (= z (R ((as const (Array Int r)) (r_ctor 0)) (mkt ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0)))))
  12 (check-sat)
  13 (assert (= (x (select (x z) 0)) (select (t1 (y z)) 1)))
  14 (check-sat)