projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: ad0b69e)
Fix strings 2.6 regression (#4413)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 29 Apr 2020 17:00:19 +0000 (12:00 -0500)
committerGitHub <noreply@github.com>
Wed, 29 Apr 2020 17:00:19 +0000 (10:00 -0700)
Fixes nightlies.

test/regress/regress1/strings/issue4379.smt2 patch | blob | history

diff --git a/test/regress/regress1/strings/issue4379.smt2 b/test/regress/regress1/strings/issue4379.smt2
index c5d024bc22be499c18be6d639d1cef2b9f786a6f..964a128fa73864c753bfc66868bc811ce5f513c8 100644 (file)
--- a/test/regress/regress1/strings/issue4379.smt2
+++ b/test/regress/regress1/strings/issue4379.smt2
@@ -5,5 +5,5 @@
 (declare-const i7 Int)
 (declare-const Str8 String)
 (declare-const Str17 String)
-(assert (distinct (str.++ "" "rvhhcn" "" Str8 (int.to.str 56)) (str.++ "" (int.to.str i7) "" Str17) Str17))
+(assert (distinct (str.++ "" "rvhhcn" "" Str8 (str.from_int 56)) (str.++ "" (str.from_int i7) "" Str17) Str17))
 (check-sat)