Fixed bug in default solve - wasn't returning when it was supposed to

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 252d18844be0ede383ecce80ed79d4f425f24ab8..82e19429224d87e9bf3e1afaae80ea5c41e722ab 100644 (file)
--- 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]) {