examples/bts/remove_unused_remove_cte.mlw

   1
   2 use int.Int
   3
   4 constant x : int
   5
   6 axiom x_spec: x >= 42
   7
   8 meta "remove_unused:dependency" axiom x_spec, constant x
   9
  10 constant y : int
  11
  12 axiom y_spec: y >= 31
  13
  14 meta "remove_unused:dependency" axiom y_spec, constant y
  15 meta "remove_unused:remove_constant" constant y
  16
  17 constant z : int
  18
  19 meta "remove_unused:remove_constant" constant z
  20
  21 goal g : forall a. a + 8 < 50