add constant regular expression check for intersection.

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index fef6cec96d37afc77d12df91ccd3e76516602661..954f8603a19ce90315cad3068596e1ad04a96a9f 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1255,7 +1255,12 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se
 }\r
 Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) {\r
   std::map< unsigned, std::set< PairNodes > > cache;\r
-  return intersectInternal(r1, r2, cache, spflag);\r
+  if(checkConstRegExp(r1) && checkConstRegExp(r2)) {\r
+    return intersectInternal(r1, r2, cache, spflag);\r
+  } else {\r
+    spflag = true;\r
+    return Node::null();\r
+  }\r
 }\r
 \r
 Node RegExpOpr::complement(Node r, int &ret) {\r