summaryrefslogtreecommitdiff
path: root/test/regress/regress2/strings
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-04-01 10:45:40 -0700
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-04-01 12:45:40 -0500
commitfe18be6fe6ac58bf6ccdb1ca18c7fae2de881aaa (patch)
treebfb3866611697b5fb3711e57adf78bd79dfee4a6 /test/regress/regress2/strings
parent995beb51ffe0334ce40391085a0d666f8e301eb3 (diff)
Move slow string regression to regress3 (#2913)
Diffstat (limited to 'test/regress/regress2/strings')
-rw-r--r--test/regress/regress2/strings/extf_d_perf.smt219
1 files changed, 0 insertions, 19 deletions
diff --git a/test/regress/regress2/strings/extf_d_perf.smt2 b/test/regress/regress2/strings/extf_d_perf.smt2
deleted file mode 100644
index 7ad094dcb..000000000
--- a/test/regress/regress2/strings/extf_d_perf.smt2
+++ /dev/null
@@ -1,19 +0,0 @@
-; COMMAND-LINE: --strings-exp --strings-fmf
-; EXPECT: sat
-(set-logic ALL)
-(declare-fun _substvar_140_ () String)
-(declare-fun _substvar_195_ () Int)
-(declare-fun _substvar_201_ () Int)
-(assert (let ((_let_0 (str.substr _substvar_140_ 10 (+ 0 (str.len _substvar_140_))))) (let ((_let_3 (str.substr _let_0 0 (str.indexof _let_0 "/" 0)))) (let ((_let_4 (str.substr _let_3 0 7))) (let ((_let_5 (str.substr _let_3 8 (+ _substvar_201_ (str.len _let_3)))))
- (and
- (str.contains _substvar_140_ "://")
- (str.contains _let_3 "@")
- (str.contains _let_5 ",")
- (not (= (str.len (str.substr _let_0 (+ 1 (str.indexof _let_0 "/" 0)) _substvar_195_)) 0))
- (not (= (str.len _let_4) 0))
- (not (str.contains _let_0 ".sock"))
- (not (str.contains _let_4 "@"))
- (not (= (str.len _let_5) 0))
- (= "mongodb://" (str.substr _substvar_140_ 0 10))))))))
-(check-sat)
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback