summaryrefslogtreecommitdiff
path: root/test/regress/regress1/strings/issue3357.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/strings/issue3357.smt2')
-rw-r--r--test/regress/regress1/strings/issue3357.smt26
1 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress1/strings/issue3357.smt2 b/test/regress/regress1/strings/issue3357.smt2
index d0e436038..6951d47e1 100644
--- a/test/regress/regress1/strings/issue3357.smt2
+++ b/test/regress/regress1/strings/issue3357.smt2
@@ -9,10 +9,10 @@
(declare-const e String)
(declare-const f String)
(assert (or
- (and (= d (str.++ e g)) (str.in.re e (re.* (str.to.re "HG4"))) (> 0 (str.to.int g)) (= 1 (str.len e)) (= 2 (str.len (str.substr b 0 (str.len d)))))
+ (and (= d (str.++ e g)) (str.in_re e (re.* (str.to_re "HG4"))) (> 0 (str.to_int g)) (= 1 (str.len e)) (= 2 (str.len (str.substr b 0 (str.len d)))))
(and
- (str.in.re (str.replace (str.replace a c "") "T" "") (re.* (re.union (str.to.re "a") (str.to.re ""))))
- (= 0 (str.to.int (str.replace (str.replace a c "") "T" "")))))
+ (str.in_re (str.replace (str.replace a c "") "T" "") (re.* (re.union (str.to_re "a") (str.to_re ""))))
+ (= 0 (str.to_int (str.replace (str.replace a c "") "T" "")))))
)
(assert (= b (str.++ d f)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback