tests/test-smoke-detector.why

   1 theory T
   2   use int.Int
   3
   4 function f (x : int) : int = x + 1
   5
   6 goal G1_true : forall x : int. f x - 1 = x
   7
   8 goal G2_false : forall x : int. f x = x
   9
  10 axiom A_false : forall x : int. f x = x
  11
  12 goal G1W : forall x : int. f x - 1 = x
  13
  14 goal G2W : forall x : int. f x = x
  15
  16 goal G3W : forall x : int. f x = 2*x
  17
  18 end