From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sun, 10 Jul 2011 16:57:38 +0000 (+0000)
Subject: Fixed bug in default solve - wasn't returning when it was supposed to
X-Git-Tag: cvc5-1.0.0~8512
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8f5e1c68701aa2a805fe656f5c580fc74b310606;p=cvc5.git

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 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]) {