summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings/regexp002.smt2
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2014-02-28 11:05:09 -0600
committerTianyi Liang <tianyi-liang@uiowa.edu>2014-02-28 22:59:00 -0600
commitacb79cbe43ddcd855db042b7c937fc2eacaa0ac3 (patch)
treee8af21bba458cbc2a00d3512519cea3e07af3b65 /test/regress/regress0/strings/regexp002.smt2
parent76f497ef9444a81143ad35b2eda899e119b8e662 (diff)
a new regular expression engine for solving both positive and negative membership constraints
Diffstat (limited to 'test/regress/regress0/strings/regexp002.smt2')
-rw-r--r--test/regress/regress0/strings/regexp002.smt21
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/regexp002.smt2 b/test/regress/regress0/strings/regexp002.smt2
index e2a44a9ab..18541af4e 100644
--- a/test/regress/regress0/strings/regexp002.smt2
+++ b/test/regress/regress0/strings/regexp002.smt2
@@ -1,5 +1,6 @@
(set-logic QF_S)
(set-info :status sat)
+(set-option :strings-exp true)
(declare-fun x () String)
(declare-fun y () String)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback