From 8f5e1c68701aa2a805fe656f5c580fc74b310606 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Sun, 10 Jul 2011 16:57:38 +0000 Subject: [PATCH] Fixed bug in default solve - wasn't returning when it was supposed to --- src/theory/theory.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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()); } 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]) { -- 2.30.2