From f7a77c4c14af25466e7ce31455a9636e0f8234e3 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 22 Feb 2018 14:08:13 -0600
Subject: Minor improvements to string rewriter (#1572)

---
 test/regress/regress1/strings/Makefile.am     |  3 ++-
 test/regress/regress1/strings/rew-020618.smt2 | 18 ++++++++++++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress1/strings/rew-020618.smt2

(limited to 'test')

diff --git a/test/regress/regress1/strings/Makefile.am b/test/regress/regress1/strings/Makefile.am
index 8ccf3f81d..400ee7cff 100644
--- a/test/regress/regress1/strings/Makefile.am
+++ b/test/regress/regress1/strings/Makefile.am
@@ -71,7 +71,8 @@ TESTS =	\
 	repl-soundness-sem.smt2 \
 	str001.smt2 \
 	str002.smt2 \
-	str007.smt2
+	str007.smt2 \
+	rew-020618.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress1/strings/rew-020618.smt2 b/test/regress/regress1/strings/rew-020618.smt2
new file mode 100644
index 000000000..5fb58a272
--- /dev/null
+++ b/test/regress/regress1/strings/rew-020618.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun s () String)
+
+(assert (or
+(= (str.++ s "A") "")
+(= (str.++ s s) "A")
+(not (str.contains s ""))
+(str.contains "" (str.++ s "A"))
+(not (= (str.replace "A" s "A") "A"))
+(not (= (str.prefixof s "A") (str.suffixof s "A")))
+(not (str.prefixof s s))
+(not (str.prefixof "" s))
+)
+)
+(check-sat)
-- 
cgit v1.2.3