test/regress/regress1/cee-bug0909-dd-scope.smt2

   1 ; COMMAND-LINE: --ee-mode=distributed
   2 ; COMMAND-LINE: --ee-mode=central
   3 ; EXPECT: sat
   4 (set-logic ALL)
   5 (set-info :status sat)
   6 (declare-datatypes ((x5 0)) (((x3) (x4))))
   7 (declare-sort x 0)
   8 (declare-sort x1 0)
   9 (declare-datatypes ((x22 0)) (((x2))))
  10 (declare-datatypes ((x2 0)) (((x2 (x2 x5) (x24 x5) (x25 Int) (x26 Int) (x27 Int)))))
  11 (declare-sort x30 0)
  12 (declare-sort x3 0)
  13 (declare-datatypes ((x4 0)) (((x44 (x43 x3)))))
  14 (declare-fun x46 (x3) x1)
  15 (declare-datatypes ((x54 0)) (((x49 (x48 x22)) (x5 (x5 x2)) (d (s x1)))))
  16 (declare-fun x5 (x22) x2)
  17 (declare-fun x67 () (Array x x54))
  18 (declare-fun x6 () (Array x x54))
  19 (declare-fun x7 () (Array x30 x4))
  20 (declare-fun x63 () x30)
  21 (declare-fun x () x)
  22 (assert (distinct x3 (ite (or (distinct x6 (store x67 x (d (x46 (x43 (select x7 x63)))))) (= x67 (store x67 x (x5 (x2 x4 x3 (x25 (x5 (x48 (select x67 x)))) (x26 (x5 (x48 (select x67 x)))) (x27 (x5 (x48 (select x6 x))))))))) x3 x4)))
  23 (check-sat)