From 1694c6b45dfa02ca22146755c89078bfa6b851ef Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 6 May 2019 06:05:19 -0700
Subject: Add support for re.all (#2980)

---
 test/regress/regress0/strings/re.all.smt2 | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test/regress/regress0/strings/re.all.smt2

(limited to 'test/regress/regress0/strings/re.all.smt2')

diff --git a/test/regress/regress0/strings/re.all.smt2 b/test/regress/regress0/strings/re.all.smt2
new file mode 100644
index 000000000..5200b924f
--- /dev/null
+++ b/test/regress/regress0/strings/re.all.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-const x String)
+(assert (str.in.re x (re.++ (str.to.re "abc") re.all)))
+(assert (not (str.prefixof "abc" x)))
+(check-sat)
-- 
cgit v1.2.3