summaryrefslogtreecommitdiff
path: root/src/cvc4.i
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2012-05-19 17:24:52 +0000
committerTim King <taking@cs.nyu.edu>2012-05-19 17:24:52 +0000
commit7a1139538caede03eb279a7b13ef7476bebd4736 (patch)
tree3d0d8eea13869c7314c3e17fa524a8d1174ae9d9 /src/cvc4.i
parentea8139dc7b727bf48bd7b7c6b169d763618a1f2a (diff)
- 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].
Diffstat (limited to 'src/cvc4.i')
-rw-r--r--src/cvc4.i1
1 files changed, 0 insertions, 1 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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback