summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClark Barrett <barrett@cs.nyu.edu>2011-07-10 19:41:04 +0000
committerClark Barrett <barrett@cs.nyu.edu>2011-07-10 19:41:04 +0000
commit587520ce888b88294fb9e4ca476e2425d8bf026e (patch)
tree97f9e9b4c73458c82a6785a55075f87b87c64e4c
parentabc169cbdba1d3fdc1400f74a4c93b747cae0575 (diff)
Reverting mistaken check-in
-rw-r--r--src/theory/theory.h4
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 82e194292..59d26ff05 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -187,9 +187,7 @@ public:
if (typeNode.getKind() == kind::TYPE_CONSTANT) {
return typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
} else {
- TheoryId id = kindToTheoryId(typeNode.getKind());
- if (id == theory::THEORY_UF) id = theory::THEORY_ARRAY;
- return id;
+ return kindToTheoryId(typeNode.getKind());
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback