Turn strings-exp off by default (for the release)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8938cd769ed36b198a9360062fe945ac5df4d328..61fdfb8c0e0f727828f8aedef1ffb7a4ee5e04b2 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -872,12 +872,14 @@ void SmtEngine::setDefaults() {
   }
 
   // set strings-exp
+  /* - disabled for 1.4 release [MGD 2014.06.25]
   if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
     if(! options::stringExp.wasSetByUser()) {
       options::stringExp.set( true );
       Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
     }
   }
+  */
   // for strings
   if(options::stringExp()) {
     if( !d_logic.isQuantified() ) {
@@ -891,6 +893,9 @@ void SmtEngine::setDefaults() {
       Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl;
     }
     if(! options::fmfBoundInt.wasSetByUser()) {
+      if(! options::fmfBoundIntLazy.wasSetByUser()) {
+        options::fmfBoundIntLazy.set( true );
+      }
       options::fmfBoundInt.set( true );
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
@@ -927,44 +932,6 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  // set strings-exp
-  if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS)) {
-    if(! options::stringExp.wasSetByUser()) {
-      options::stringExp.set(true);
-      Trace("smt") << "turning on strings-exp, for the theory of strings" << 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()) {
-      if(! options::fmfBoundIntLazy.wasSetByUser()) {
-        options::fmfBoundIntLazy.set( true );
-      }
-      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
   if(! options::ufSymmetryBreaker.wasSetByUser()) {
     bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();

diff --git a/test/regress/regress0/strings/artemis-0512-nonterm.smt2 b/test/regress/regress0/strings/artemis-0512-nonterm.smt2
index ed97f36dd4f6496f2c8412aaf2e0853f12c85ec9..4b1cad8f620f928840864c66c87a4909b7f12923 100644 (file)
--- a/test/regress/regress0/strings/artemis-0512-nonterm.smt2
+++ b/test/regress/regress0/strings/artemis-0512-nonterm.smt2
@@ -1,4 +1,5 @@
 (set-logic QF_S)
+(set-option :strings-exp true)
 (set-info :status unsat)
 
 (declare-const Y String)

diff --git a/test/regress/regress0/strings/leadingzero001.smt2 b/test/regress/regress0/strings/leadingzero001.smt2
index 3987c92ac7d0a092a7f4e227f84c1acd1c44f078..ae61b5f5b709df7d728516cc09ca0a4ef86d1b39 100644 (file)
--- a/test/regress/regress0/strings/leadingzero001.smt2
+++ b/test/regress/regress0/strings/leadingzero001.smt2
@@ -1,4 +1,5 @@
 (set-logic QF_S)\r
+(set-option :strings-exp true)\r
 (set-info :status sat)\r
 \r
 (declare-fun Y () String)\r

diff --git a/test/regress/regress0/strings/reloop.smt2 b/test/regress/regress0/strings/reloop.smt2
index f5460712145640d14fc5f560ae4c5f379458ca62..39b2b76b1159628b21bf946f0bb99b6b1c9266bf 100644 (file)
--- a/test/regress/regress0/strings/reloop.smt2
+++ b/test/regress/regress0/strings/reloop.smt2
@@ -1,4 +1,5 @@
 (set-logic QF_S)\r
+(set-option :strings-exp true)\r
 (set-info :status sat)\r
 \r
 (declare-fun x () String)\r