diff --git a/drivers/cvc4_14.drv b/drivers/cvc4_14.drv index 217728946de47e41c8ba0a86944f95055dd28c3f..a5b85691e2f741716af76db1cee6383ce3507478 100644 --- a/drivers/cvc4_14.drv +++ b/drivers/cvc4_14.drv @@ -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" diff --git a/drivers/z3_432.drv b/drivers/z3_432.drv index a6892ef5484e6b9315813f4b58cd659916efae65..f7098d50ee36cc856236aa94b308c61227e0e4fa 100644 --- a/drivers/z3_432.drv +++ b/drivers/z3_432.drv @@ -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"