Commit 7a62e628 authored by François Bobot's avatar François Bobot

Revert "cvc3 understand definition"

 - When the encoding can't encode a definition it transform it into an
   axiom. But it's not the same than before. The differences is that
   eliminate algebraic is before this transformation into axiom and
   not after. So if the definition start with a match, in one case
   that give different nice axioms, and in the other case that
   introduce a match function which is polymorph and not well used by
   provers.

   Possible solutions :
   1) make the match function easier to use with some modification to
   its definition and discriminate it.
   2) Eliminate the match function when the encoding tranform a
   definition into axioms.

This reverts commit 1f652980.
parent 3ef231cd
......@@ -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