type conversion

1 files changed, 7 insertions, 1 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ef4f01cd1..dcca1624d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -954,10 +954,16 @@ void SmtEngine::setLogicInternal() throw() {
       options::fmfBoundInt.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
+	if(! options::rewriteDivk.wasSetByUser()) {
+      options::rewriteDivk.set( true );
+      Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
+    }
+
+	/*
     if(! options::stringFMF.wasSetByUser()) {
       options::stringFMF.set( true );
       Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
-    }
+    }*/
   }
 
   // by default, symmetry breaker is on only for QF_UF