Add a benchmark that detects a bug in parsing. Thank Vijay for his bug report.

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index e7b3f2277313cf7c394d71690d64cc7e207f7786..dd3c6b53a2f94691723f5fd05fb1fab13f4185c2 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -20,6 +20,7 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 TESTS =        \
   at001.smt2 \
+  bug001.smt2 \
   cardinality.smt2 \
   escchar.smt2 \
   str001.smt2 \

diff --git a/test/regress/regress0/strings/bug001.smt2 b/test/regress/regress0/strings/bug001.smt2
new file mode 100644 (file)
index 0000000..4956832
--- /dev/null
+++ b/test/regress/regress0/strings/bug001.smt2
@@ -0,0 +1,15 @@
+(set-logic QF_S)\r
+(set-info :status sat)\r
+\r
+(declare-fun x () String)\r
+(declare-fun y () String)\r
+(declare-fun z () String)\r
+\r
+(assert (= "\x4a" x))\r
+(assert (= "\x6a" y))\r
+\r
+(assert (= "\x4A" z))\r
+\r
+(assert (= x z))\r
+\r
+(check-sat)\r