update drivers wrt the last commit

bench/valid/int.why

@@ -2,4 +2,14 @@ theory Test
   use import int.Int
   goal G1 : 5 * 10 = 50
   goal G2 : forall x:int. x + x - x + x  = 2 * x
+
+  goal CompatOrderAdd  : forall x y z : int. x <= y -> x + z <= y + z
+  goal CompatOrderMult : forall x y z : int. x <= y -> 0 <= z -> x * z <= y * z
+
+  goal InvMult : forall x y : int. (-x) * y = - (x * y) = x * (-y)
+  goal InvSquare : forall x : int. x * x = (-x) * (-x)
+  goal ZeroMult : forall x : int. x * 0 = 0 = 0 * x
+  goal SquareNonNeg1 : forall x : int. x <= 0 -> 0 <= x * x
+  goal SquareNonNeg : forall x : int. 0 <= x * x
+  goal ZeroLessOne : 0 <= 1
 end

drivers/alt_ergo.drv

@@ -59,6 +59,8 @@ theory int.Int
   remove prop Trans
   remove prop Total
   remove prop Antisymm
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
 
 end
 
@@ -102,6 +104,8 @@ theory real.Real
   remove prop Total
   remove prop Antisymm
   remove prop Inverse
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
 
 end
 

drivers/coq.drv

@@ -72,6 +72,10 @@ theory int.Int
   remove prop Trans
   remove prop Antisymm
   remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop CompatOrderMult
+
 end
 
 theory int.Abs
@@ -125,6 +129,9 @@ theory real.Real
   remove prop Comm.Comm
   remove prop Unitary
   remove prop Inverse
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop CompatOrderMult
 
 end
 

drivers/cvc3.drv

@@ -58,6 +58,8 @@ theory int.Int
   remove prop Trans
   remove prop Antisymm
   remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
 
   meta "encoding : kept" type int
 
@@ -96,6 +98,8 @@ theory real.Real
   remove prop Trans
   remove prop Antisymm
   remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
 
   meta "encoding : kept" type real
 

drivers/simplify.drv

@@ -62,6 +62,8 @@ theory int.Int
   remove prop Trans
   remove prop Antisymm
   remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
 
   (* use with explicit polymorphism *)
   meta "enco_poly" "explicit"

drivers/z3.drv

@@ -58,6 +58,8 @@ theory int.Int
   remove prop Trans
   remove prop Antisymm
   remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
 
   meta "encoding : kept" type int
 
@@ -96,6 +98,8 @@ theory real.Real
   remove prop Trans
   remove prop Antisymm
   remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
 
   meta "encoding : kept" type real