2 files changed, 0 insertions, 16 deletions
diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index e9bfde024..fa42e0b28 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -331,14 +331,6 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
       status = doCommand(smt, *subcmd, options) && status;
     }
   } else {
-    // by default, symmetry breaker is on only for QF_UF
-    if(! options.ufSymmetryBreakerSetByUser) {
-      SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
-      if(logic != NULL) {
-        options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF");
-      }
-    }
-
     if(options.verbosity > 0) {
       *options.out << "Invoking: " << *cmd << endl;
     }
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index 5c8f908f8..7b0c70a8a 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -655,14 +655,6 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
       status = doCommand(smt, *subcmd, options) && status;
     }
   } else {
-    // by default, symmetry breaker is on only for QF_UF
-    if(! options.ufSymmetryBreakerSetByUser) {
-      SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
-      if(logic != NULL) {
-        options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF");
-      }
-    }
-
     if(options.verbosity > 0) {
       *options.out << "Invoking: " << *cmd << endl;
     }