minor fix

3 files changed, 6 insertions, 3 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index df2364790..ade34a1f1 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -505,6 +505,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
   // assert the (relevant) portion of the equality engine to the model
   if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
   {
+    Trace("strings-model") << "TheoryStrings : assertEqualityEngine ---> :(" << std::endl;
     return false;
   }
 
@@ -1646,7 +1647,7 @@ void TheoryStrings::checkExtfEval( int effort ) {
             Trace("strings-extf") << "  resolve extf : " << sn << " -> " << nrc << std::endl;
             d_im.sendInference(
                 einfo.d_exp, conc, effort == 0 ? "EXTF" : "EXTF-N", true);
-            if (!d_state.isInConflict())
+            if (d_state.isInConflict())
             {
               Trace("strings-extf-debug") << "  conflict, return." << std::endl;
               return;
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index dd5f98db1..1b877e0e7 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -363,6 +363,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero));
     conc2.push_back(lem);
 
+    lem = nm->mkNode(GEQ, stoit, d_zero);
+    conc2.push_back(lem);
+
     /*
     lem = d_empty_str.eqNode(nm->mkNode(APPLY_UF, us, lens));
     conc2.push_back(lem);
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index bd570b446..281df2d33 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1691,8 +1691,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
           nm->mkNode(AND, nm->mkNode(LEQ, zero, c), nm->mkNode(LT, c, ten)),
           c,
           negOne);
-    }
-    */
+    }*/
   }
   else if (nk == kind::STRING_IN_REGEXP)
   {