Skip to content

GitLab

Commit 980d71b6 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Use transformation detect_polymorphism by CVC4 >= 1.4 and Z3 >= 4.3.2

parent cc12740c
Hide whitespace changes
Inline Side-by-side
drivers/cvc4_14.drv
View file @ 980d71b6
......@@ -18,10 +18,13 @@ import "discrimination.gen"
transformation "inline_trivial"
transformation "eliminate_builtin"
(* temporarily disabled: too much experimental
transformation "detect_polymorphism"
transformation "eliminate_definition"
(* We could keep more definitions by using
transformation "eliminate_definition_if_poly"
instead, but some proofs are lost
(examples/logic/triangle_inequality.why)
*)
transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"
......
drivers/z3_432.drv
View file @ 980d71b6
......@@ -10,10 +10,13 @@ import "discrimination.gen"
transformation "inline_trivial"
transformation "eliminate_builtin"
(* temporarily disabled: too much experimental
transformation "detect_polymorphism"
transformation "eliminate_definition"
(* We could keep more definitions by using
transformation "eliminate_definition_if_poly"
instead, but some proofs are lost
(examples/logic/triangle_inequality.why)
*)
transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"
......
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