summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp7
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback