diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2011-07-10 16:57:38 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2011-07-10 16:57:38 +0000 |
commit | 8f5e1c68701aa2a805fe656f5c580fc74b310606 (patch) | |
tree | dbb4913bba68fce8b51fb7fe50b574374f938ed3 /src | |
parent | 9f32d1b91b593891037e5f8f0c107a1c3d3d9d16 (diff) |
Fixed bug in default solve - wasn't returning when it was supposed to
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 252d18844..82e194292 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -187,7 +187,9 @@ public: if (typeNode.getKind() == kind::TYPE_CONSTANT) { return typeConstantToTheoryId(typeNode.getConst<TypeConstant>()); } else { - return kindToTheoryId(typeNode.getKind()); + TheoryId id = kindToTheoryId(typeNode.getKind()); + if (id == theory::THEORY_UF) id = theory::THEORY_ARRAY; + return id; } } @@ -428,6 +430,7 @@ public: } if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { outSubstitutions.addSubstitution(in[1], in[0]); + return SOLVE_STATUS_SOLVED; } if (in[0].getMetaKind() == kind::metakind::CONSTANT && in[1].getMetaKind() == kind::metakind::CONSTANT) { if (in[0] != in[1]) { |