From: ajreynol <reynolds@larapc05.epfl.ch>
Date: Fri, 13 Jun 2014 15:18:05 +0000 (+0200)
Subject: Fix handling of ALIA.
X-Git-Tag: cvc5-1.0.0~6821
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=57e44de6cc08f36743fe46a2ae4ff8810029e5c4;p=cvc5.git

Fix handling of ALIA.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6ab25ee57..6b7bf424f 100644
--- 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);