Simplification of the preregister and register throught a NodeVisitor class. The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class.

1 files changed, 6 insertions, 1 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fe5628dd0..60030bbab 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -249,7 +249,12 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
     throw ModalException("logic already set");
   }
   d_logic = s;
-  d_theoryEngine->d_logic = s;
+  d_theoryEngine->setLogic(s);
+
+  // If in arrays, set the UF handler to arrays
+  if (s == "QF_AX") {
+    theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY);
+  }
 }
 
 void SmtEngine::setInfo(const std::string& key, const SExpr& value)