test/regress/regress0/print_model.cvc

   1 % COMMAND-LINE: --produce-models
   2 % EXPECT: sat
   3 % EXPECT: MODEL BEGIN
   4 % EXPECT: s1 : INT = 2;
   5 % EXPECT: s2 : INT = 1;
   6 % EXPECT: MODEL END;
   7
   8 OPTION "produce-models";
   9 s1, s2 : INT;
  10 ASSERT s1 = 2;
  11 CHECKSAT s2 > 0 AND s2 < s1;
  12 COUNTERMODEL;