Squashed commit of the following:

 * Fix a bug in intersection
 * merging...
 * add delayed length lemmas
 * PreRegisterTerm is changed.
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.
 * add delayed length lemmas
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.

1 files changed, 11 insertions, 0 deletions

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 18df0f759..092c7e166 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1220,6 +1220,17 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se
         cset.clear();
         firstChars(r1, cset, vset);
         std::vector< Node > vec_nodes;
+        Node delta_exp;
+        int flag = delta(r1, delta_exp);
+        int flag2 = delta(r2, delta_exp);
+        if(flag != 2 && flag2 != 2) {
+          if(flag == 1 && flag2 == 1) {
+            vec_nodes.push_back(d_emptySingleton);
+          } else {
+            //TODO
+            spflag = true;
+          }
+        }
         for(std::set<unsigned>::const_iterator itr = cset.begin();
           itr != cset.end(); itr++) {
           CVC4::String c( CVC4::String::convertUnsignedIntToChar(*itr) );