From d40b8aa4354c8b52845b1b560d3fe4f482138623 Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 12 May 2014 11:10:06 -0500
Subject: Add a benchmark that detects a bug in parsing. Thank Vijay for his
 bug report.

---
 test/regress/regress0/strings/Makefile.am |  1 +
 test/regress/regress0/strings/bug001.smt2 | 15 +++++++++++++++
 2 files changed, 16 insertions(+)
 create mode 100644 test/regress/regress0/strings/bug001.smt2

(limited to 'test/regress')

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index e7b3f2277..dd3c6b53a 100644
--- 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
index 000000000..49568329e
--- /dev/null
+++ b/test/regress/regress0/strings/bug001.smt2
@@ -0,0 +1,15 @@
+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= "\x4a" x))
+(assert (= "\x6a" y))
+
+(assert (= "\x4A" z))
+
+(assert (= x z))
+
+(check-sat)
-- 
cgit v1.2.3