From 37011fff190bd87adc9d501b6bda48942321aa6d Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 7 Jan 2015 10:50:58 -0600
Subject: bug fix, thanks to Pierre's report

---
 test/regress/regress0/strings/Makefile.am |  1 +
 test/regress/regress0/strings/bug002.smt2 | 10 ++++++++++
 2 files changed, 11 insertions(+)
 create mode 100644 test/regress/regress0/strings/bug002.smt2

(limited to 'test/regress/regress0/strings')

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 8a2674cee..414904919 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -21,6 +21,7 @@ MAKEFLAGS = -k
 TESTS =	\
   at001.smt2 \
   bug001.smt2 \
+  bug002.smt2 \
   cardinality.smt2 \
   escchar.smt2 \
   escchar_25.smt2 \
diff --git a/test/regress/regress0/strings/bug002.smt2 b/test/regress/regress0/strings/bug002.smt2
new file mode 100644
index 000000000..15d1ea5a2
--- /dev/null
+++ b/test/regress/regress0/strings/bug002.smt2
@@ -0,0 +1,10 @@
+(set-logic ASLIA)
+(set-info :smt-lib-version 2.0)
+(set-option :strings-exp true)
+(set-info :status sat)
+
+; regex = [\*-,\t\*-\|](.{6,}()?)+
+(define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.loop re.allchar 6 ) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) )  ) )
+(assert (not (strinre "6O\1\127\n?")))
+
+(check-sat)
\ No newline at end of file
-- 
cgit v1.2.3