From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 12 May 2014 16:10:06 +0000 (-0500)
Subject: Add a benchmark that detects a bug in parsing. Thank Vijay for his bug report.
X-Git-Tag: cvc5-1.0.0~6911
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d40b8aa4354c8b52845b1b560d3fe4f482138623;p=cvc5.git

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 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)