Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases for division by 0.

1 files changed, 9 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7fcb64219..24d6fb0b4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -661,6 +661,15 @@ void SmtEngine::setLogicInternal() throw() {
 
   d_logic.lock();
 
+  // may need to force uninterpreted functions to be on for non-linear
+  if(d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
+     !d_logic.isLinear() &&
+     !d_logic.isTheoryEnabled(theory::THEORY_UF)){
+    d_logic = d_logic.getUnlockedCopy();
+    d_logic.enableTheory(theory::THEORY_UF);
+    d_logic.lock();
+  }
+
   // Set the options for the theoryOf
   if(!options::theoryOfMode.wasSetByUser()) {
     if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) {