summaryrefslogtreecommitdiff
path: root/test/regress/regress1/strings/rew-check1.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/strings/rew-check1.smt2')
-rw-r--r--test/regress/regress1/strings/rew-check1.smt26
1 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress1/strings/rew-check1.smt2 b/test/regress/regress1/strings/rew-check1.smt2
index 5cb85e4ca..2de2c5747 100644
--- a/test/regress/regress1/strings/rew-check1.smt2
+++ b/test/regress/regress1/strings/rew-check1.smt2
@@ -1,10 +1,10 @@
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
(set-logic ALL)
(set-info :status unsat)
(declare-fun x () String)
(assert (not (=
-(str.in.re x (re.++ (re.* re.allchar ) (str.to.re "A") (re.* re.allchar ) re.allchar (re.* re.allchar ) (re.* (str.to.re "A")) (re.* re.allchar )))
-(str.in.re x (re.++ (re.* (str.to.re "A")) (re.* (str.to.re "B")) (re.* re.allchar ) (str.to.re "A") (re.* re.allchar ) re.allchar (re.* re.allchar )))
+(str.in_re x (re.++ (re.* re.allchar ) (str.to_re "A") (re.* re.allchar ) re.allchar (re.* re.allchar ) (re.* (str.to_re "A")) (re.* re.allchar )))
+(str.in_re x (re.++ (re.* (str.to_re "A")) (re.* (str.to_re "B")) (re.* re.allchar ) (str.to_re "A") (re.* re.allchar ) re.allchar (re.* re.allchar )))
)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback