summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings/loop008.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/loop008.smt2
parent76f497ef9444a81143ad35b2eda899e119b8e662 (diff)
a new regular expression engine for solving both positive and negative membership constraints
Diffstat (limited to 'test/regress/regress0/strings/loop008.smt2')
-rw-r--r--test/regress/regress0/strings/loop008.smt21
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/loop008.smt2 b/test/regress/regress0/strings/loop008.smt2
index 91ed8cdf0..113577e48 100644
--- a/test/regress/regress0/strings/loop008.smt2
+++ b/test/regress/regress0/strings/loop008.smt2
@@ -1,4 +1,5 @@
(set-logic QF_S)
+(set-option :strings-exp true)
(set-info :status sat)
(declare-fun x () String)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback