Merge branch 'master' of https://github.com/CVC4/CVC4

1 files changed, 20 insertions, 20 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 46843b21a..c77c05423 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -943,26 +943,26 @@ void SmtEngine::setLogicInternal() throw() {
   }
 
 
-  //for strings
-  if(options::stringExp.wasSetByUser()) {
-	  if( !d_logic.isQuantified() ) {
-		  d_logic = d_logic.getUnlockedCopy();
-		  d_logic.enableQuantifiers();
-		  d_logic.lock();
-		  Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl;
-	  }
-	  if(! options::finiteModelFind.wasSetByUser()) {
-		  options::finiteModelFind.set( true );
-		  Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
-	  }
-	  if(! options::fmfBoundInt.wasSetByUser()) {
-		  options::fmfBoundInt.set( true );
-		  Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
-	  }
-	  if(! options::stringFMF.wasSetByUser()) {
-		options::stringFMF.set( true );
-		Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
-	  }
+  // for strings
+  if(options::stringExp()) {
+    if( !d_logic.isQuantified() ) {
+      d_logic = d_logic.getUnlockedCopy();
+      d_logic.enableQuantifiers();
+      d_logic.lock();
+      Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl;
+    }
+    if(! options::finiteModelFind.wasSetByUser()) {
+      options::finiteModelFind.set( true );
+      Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
+    }
+    if(! options::fmfBoundInt.wasSetByUser()) {
+      options::fmfBoundInt.set( true );
+      Trace("smt") << "turning on fmf-bound-int, 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