Fix handling of ALIA.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6ab25ee5719c480910c97b135b95021a836151df..6b7bf424f819305974d4be7d3c286d1fba9c7458 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -980,7 +980,8 @@ void SmtEngine::setDefaults() {
   }
 
   // If in arrays, set the UF handler to arrays
-  if(d_logic.isTheoryEnabled(THEORY_ARRAY) && !d_logic.isQuantified()) {
+  if(d_logic.isTheoryEnabled(THEORY_ARRAY) && ( !d_logic.isQuantified() || 
+     (d_logic.isQuantified() && !d_logic.isTheoryEnabled(THEORY_UF)))) {
     Theory::setUninterpretedSortOwner(THEORY_ARRAY);
   } else {
     Theory::setUninterpretedSortOwner(THEORY_UF);