projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 6710b08)
Add strings-exp to regression (#4923)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 20 Aug 2020 00:02:48 +0000 (19:02 -0500)
committerGitHub <noreply@github.com>
Thu, 20 Aug 2020 00:02:48 +0000 (19:02 -0500)
str.at expands to str.substr, thus this benchmark (may) require strings-exp if things do not rewrite/preprocess. This triggers a regress0 failure on proof-new currently.

test/regress/regress0/strings/unsound-0908.smt2 patch | blob | history

diff --git a/test/regress/regress0/strings/unsound-0908.smt2 b/test/regress/regress0/strings/unsound-0908.smt2
index 9c91d135f3f2f6f1ca4e18927098c9a2e253de46..632c6713d1cae97b3cfd406771e5f2dbf1a931fd 100644 (file)
--- a/test/regress/regress0/strings/unsound-0908.smt2
+++ b/test/regress/regress0/strings/unsound-0908.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
 (set-logic QF_SLIA)
 (set-info :status sat)
 (declare-const x String)