test/regress/regress0/boolean-terms.cvc

   1 % EXPECT: sat
   2 %OPTION "produce-models";
   3
   4 f : BOOLEAN -> INT;
   5 x : INT;
   6 p : BOOLEAN -> BOOLEAN;
   7
   8 ASSERT f(p(TRUE)) = x;
   9 ASSERT f(p(FALSE)) = x + 1;
  10
  11 CHECKSAT;
  12 %GET_VALUE f(p(TRUE));
  13 %GET_VALUE f(p(TRUE)) = x;
  14 %GET_VALUE f(p(FALSE)) = x + 1;
  15 %COUNTERMODEL;