diff options
| author | ajreynol <reynolds@larapc05.epfl.ch> | 2014-06-13 17:18:05 +0200 |
|---|---|---|
| committer | ajreynol <reynolds@larapc05.epfl.ch> | 2014-06-13 17:18:05 +0200 |
| commit | 57e44de6cc08f36743fe46a2ae4ff8810029e5c4 (patch) | |
| tree | d421932100e95941b009fb63a56975a5b88c6001 /src/smt | |
| parent | 46e95393e39eca02a7f1e69bd343b6286eddd5c4 (diff) | |
Fix handling of ALIA.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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); |