diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress2/strings/extf_d_perf.smt2 | 19 |
2 files changed, 20 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e0e57acf9..f22796929 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1729,6 +1729,7 @@ set(regress_2_tests regress2/strings/cmu-disagree-0707-dd.smt2 regress2/strings/cmu-prereg-fmf.smt2 regress2/strings/cmu-repl-len-nterm.smt2 + regress2/strings/extf_d_perf.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/norn-dis-0707-3.smt2 diff --git a/test/regress/regress2/strings/extf_d_perf.smt2 b/test/regress/regress2/strings/extf_d_perf.smt2 new file mode 100644 index 000000000..7ad094dcb --- /dev/null +++ b/test/regress/regress2/strings/extf_d_perf.smt2 @@ -0,0 +1,19 @@ +; 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) + |