From 22acfb03456d5816c550d822ef7e27d147475eee Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 5 May 2014 18:01:14 -0500
Subject: [PATCH] add constant regular expression check for intersection.

---
 src/theory/strings/regexp_operation.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index fef6cec96..954f8603a 100644
--- 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
 }
 Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) {
   std::map< unsigned, std::set< PairNodes > > cache;
-  return intersectInternal(r1, r2, cache, spflag);
+  if(checkConstRegExp(r1) && checkConstRegExp(r2)) {
+    return intersectInternal(r1, r2, cache, spflag);
+  } else {
+    spflag = true;
+    return Node::null();
+  }
 }
 
 Node RegExpOpr::complement(Node r, int &ret) {
-- 
2.30.2