alt_ergo_2_2_0.drv

(* Driver for Alt-Ergo versions >= 0.95.2 *)

prelude "(* this is the prelude for Alt-Ergo, version >= 0.95.2 and <= 2.2.0 *)"


transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"

transformation "split_premise_right"
transformation "simplify_formula"


import "alt_ergo_common.drv"
import "no-bv.gen"

(* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
valid "^Inconsistent assumption$"