bugfix, enable only QF_LRA, not other arith

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b9c15ac71e0b142ead1665a95300dbda883ae95c..97046a1ae8d40077be0323a5e4fb291fb6d55d46 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -573,7 +573,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
        ) ||
       // QF_LRA
       (not d_logic.isQuantified() &&
-       d_logic.isPure(THEORY_ARITH)
+       d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
        ) ||
       // Quantifiers
       d_logic.isQuantified()
@@ -589,7 +589,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
        ) ||
       // QF_LRA
       (not d_logic.isQuantified() &&
-       d_logic.isPure(THEORY_ARITH)
+       d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
        ) ||
       // Quantifiers
       d_logic.isQuantified()