Commit 7a5eb927 authored by Andrei Paskevich's avatar Andrei Paskevich

fully eliminate definitions for Z3 and CVC3

until we understand why keeping them makes nightlies regress
parent 3f213834
......@@ -14,7 +14,7 @@ time "why3cpulimit time : %s s"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
......
......@@ -16,7 +16,7 @@ time "why3cpulimit time : %s s"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment