drivers/alt_ergo_2_2_0.drv

   1 (* Driver for Alt-Ergo versions >= 0.95.2 *)
   2
   3 prelude "(* this is the prelude for Alt-Ergo, version >= 0.95.2 and <= 2.2.0 *)"
   4
   5 filename "%f-%t-%g.why"
   6
   7 (* Performed introductions depending on whether counterexamples are
   8    requested, as said by the meta "get_counterexmp". When this meta
   9    set, this transformation introduces the model variables that are
  10    still embedded in the goal. When it is not set, it removes all
  11    these unused-ce-related variables, even in the context.  *)
  12 transformation "counterexamples_dependent_intros"
  13
  14 transformation "inline_trivial"
  15
  16 transformation "eliminate_builtin"
  17 transformation "eliminate_recursion"
  18 transformation "eliminate_inductive"
  19 transformation "eliminate_if"
  20 transformation "eliminate_epsilon"
  21 transformation "eliminate_algebraic"
  22 transformation "eliminate_literal"
  23 transformation "eliminate_let"
  24
  25 transformation "split_premise_right"
  26 transformation "simplify_formula"
  27
  28
  29 import "alt_ergo_common.drv"
  30 import "no-bv.gen"
  31
  32 (* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
  33 valid "^Inconsistent assumption$"