- The array type rules were fixed to use isSubtypeOf.

- The type of (kind::DIVISION x y) is RealType.
- A reference to util/pseudoboolean.i was removed.
- rec5.cvc is disabled for now.  The type of 2 is Integer which is not a subtype of [0..11].

3 files changed, 9 insertions, 7 deletions

diff --git a/src/cvc4.i b/src/cvc4.i
index 8505d5128..ce4639137 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -103,7 +103,6 @@ using namespace CVC4;
 %include "util/bitvector.i"
 %include "util/subrange_bound.i"
 %include "util/array.i"
-%include "util/pseudoboolean.i"
 %include "util/hash.i"
 
 %include "expr/type.i"
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index af358b00d..7a8e0fab4 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -64,7 +64,8 @@ public:
         }
       }
     }
-    return (isInteger ? integerType : realType);
+    bool isDivision = n.getKind() == kind::DIVISION;
+    return (isInteger && !isDivision ? integerType : realType);
   }
 };/* class ArithOperatorTypeRule */
 
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index fabff0aab..ccbb37936 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -35,7 +35,7 @@ struct ArraySelectTypeRule {
         throw TypeCheckingExceptionPrivate(n, "array select operating on non-array");
       }
       TypeNode indexType = n[1].getType(check);
-      if(arrayType.getArrayIndexType() != indexType) {
+      if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
         throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
       }
     }
@@ -54,10 +54,12 @@ struct ArrayStoreTypeRule {
       }
       TypeNode indexType = n[1].getType(check);
       TypeNode valueType = n[2].getType(check);
-      if(arrayType.getArrayIndexType() != indexType) {
+      if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
         throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
       }
-      if(arrayType.getArrayConstituentType() != valueType) {
+      if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){
+	Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl;
+	Debug("array-types") << "value types: " << valueType << std::endl;
         throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
       }
     }
@@ -79,11 +81,11 @@ struct ArrayTableFunTypeRule {
         throw TypeCheckingExceptionPrivate(n, "array table fun arg 1 is non-array");
       }
       TypeNode indexType = n[2].getType(check);
-      if(arrayType.getArrayIndexType() != indexType) {
+      if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
         throw TypeCheckingExceptionPrivate(n, "array table fun arg 2 does not match type of array");
       }
       indexType = n[3].getType(check);
-      if(arrayType.getArrayIndexType() != indexType) {
+      if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
         throw TypeCheckingExceptionPrivate(n, "array table fun arg 3 does not match type of array");
       }
     }