summaryrefslogtreecommitdiff
path: root/test/regress/regress1/strings/double-replace.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/strings/double-replace.smt2')
-rw-r--r--test/regress/regress1/strings/double-replace.smt23
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/regress1/strings/double-replace.smt2 b/test/regress/regress1/strings/double-replace.smt2
index 0800592d6..bfbc3afc1 100644
--- a/test/regress/regress1/strings/double-replace.smt2
+++ b/test/regress/regress1/strings/double-replace.smt2
@@ -1,7 +1,8 @@
(set-logic SLIA)
+(set-option :strings-fmf true)
(set-option :strings-exp true)
(set-info :status sat)
(declare-fun x () String)
(declare-fun y () String)
(assert (not (= (str.replace (str.replace x y x) x y) x)))
-(check-sat) \ No newline at end of file
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback