1 files changed, 0 insertions, 10 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 899da4d4a..e06363883 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1097,11 +1097,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     {
       options::quantSplit.set(false);
     }
-    // rewrite divk
-    if (!options::rewriteDivk.wasSetByUser())
-    {
-      options::rewriteDivk.set(true);
-    }
     // do not do macros
     if (!options::macrosQuant.wasSetByUser())
     {
@@ -1136,11 +1131,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   }
   if (options::cegqi())
   {
-    // must rewrite divk
-    if (!options::rewriteDivk.wasSetByUser())
-    {
-      options::rewriteDivk.set(true);
-    }
     if (options::incrementalSolving())
     {
       // cannot do nested quantifier elimination in incremental mode