summaryrefslogtreecommitdiff
path: root/src/theory/strings/regexp_operation.h
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2014-10-21 23:10:35 -0500
committerTianyi Liang <tianyi-liang@uiowa.edu>2014-10-21 23:10:35 -0500
commit58e47f72906773748183a141f314a21f5b970b0b (patch)
treeda9291c5a54509318d580b486242091381ff7dcc /src/theory/strings/regexp_operation.h
parentff3efb7f258c04a3371e28da3558451a4c81f000 (diff)
Fixed bug 589
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
-rw-r--r--src/theory/strings/regexp_operation.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 2ae578cd6..ce3093528 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -22,6 +22,7 @@
#include <vector>
#include <set>
#include <algorithm>
+#include <climits>
#include "util/hash.h"
#include "util/regexp.h"
#include "theory/theory.h"
@@ -46,6 +47,7 @@ private:
Node d_emptyRegexp;
Node d_zero;
Node d_one;
+ CVC4::Rational RMAXINT;
char d_char_start;
char d_char_end;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback