test/regress/regress0/bug522.smt2

   1 ; EXPECT: sat
   2 ; EXPECT: sat
   3 (set-option :incremental "true")
   4 (set-logic QF_UF)
   5
   6 (push 1)
   7 (declare-sort U 0)
   8 (declare-fun x () U)
   9 (declare-fun y () U)
  10 (assert (= x y))
  11 (check-sat)
  12 (pop 1)
  13
  14 (check-sat)