why3 driver should ignore polymorphism of equality

c8bbcd4b · MARCHE Claude · b48938dc · c8bbcd4b
Commit c8bbcd4b authored May 30, 2016 by MARCHE Claude
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 0 deletions

drivers/why3.drv drivers/why3.drv +1 -0

No files found.
--- a/drivers/why3.drv
+++ b/drivers/why3.drv
@@ -7,4 +7,5 @@ theory BuiltIn
  syntax type  int  "int"
  syntax type  real "real"
  syntax predicate (=)  "(%1 = %2)"
+  meta "encoding:ignore_polymorphism_ls" predicate (=)
 end