test/regress/regress0/bug595.cvc

   1 % EXPECT: sat
   2
   3 f : INT -> [# i:INT, b:INT #];
   4 a : INT;
   5 ASSERT f(a) /= (# i := 0, b := 0 #);
   6
   7 CHECKSAT;