protect integers even if int.Int is not used

drivers/cvc3.drv

@@ -28,6 +28,8 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(= %1 %2)"
+
+  meta "encoding : kept" type int
 end
 
 theory int.Int
@@ -62,8 +64,6 @@ theory int.Int
   remove prop NonTrivialRing
   remove prop CompatOrderAdd
 
-  meta "encoding : kept" type int
-
 end
 
 

drivers/verit.drv

@@ -28,6 +28,8 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(= %1 %2)"
+
+  meta "encoding : kept" type int
 end
 
 theory int.Int
@@ -62,8 +64,6 @@ theory int.Int
   remove prop NonTrivialRing
   remove prop CompatOrderAdd
 
-  meta "encoding : kept" type int
-
 end
 
 

drivers/yices.drv

@@ -28,6 +28,8 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(= %1 %2)"
+
+  meta "encoding : kept" type int
 end
 
 theory int.Int
@@ -62,8 +64,6 @@ theory int.Int
   remove prop NonTrivialRing
   remove prop CompatOrderAdd
 
-  meta "encoding : kept" type int
-
 end
 
 

drivers/z3.drv

@@ -29,6 +29,8 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(= %1 %2)"
+
+  meta "encoding : kept" type int
 end
 
 theory int.Int
@@ -63,8 +65,6 @@ theory int.Int
   remove prop NonTrivialRing
   remove prop CompatOrderAdd
 
-  meta "encoding : kept" type int
-
 end
 
 

drivers/z3_array.drv

@@ -29,6 +29,8 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(= %1 %2)"
+
+  meta "encoding : kept" type int
 end
 
 theory int.Int
@@ -63,8 +65,6 @@ theory int.Int
   remove prop NonTrivialRing
   remove prop CompatOrderAdd
 
-  meta "encoding : kept" type int
-
 end
 
 

drivers/z3_smtv2.drv

@@ -30,6 +30,8 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(= %1 %2)"
+
+  meta "encoding : kept" type int
 end
 
 theory int.Int
@@ -64,8 +66,6 @@ theory int.Int
   remove prop NonTrivialRing
   remove prop CompatOrderAdd
 
-  meta "encoding : kept" type int
-
 end
 
 

drivers/z3_smtv2_array.drv

@@ -31,6 +31,8 @@ theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(= %1 %2)"
+
+  meta "encoding : kept" type int
 end
 
 theory int.Int
@@ -65,8 +67,6 @@ theory int.Int
   remove prop NonTrivialRing
   remove prop CompatOrderAdd
 
-  meta "encoding : kept" type int
-
 end