test/regress/regress0/bug596.cvc

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