diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress1/bug590.smt2 | |
parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress1/bug590.smt2')
-rw-r--r-- | test/regress/regress1/bug590.smt2 | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/test/regress/regress1/bug590.smt2 b/test/regress/regress1/bug590.smt2 new file mode 100644 index 000000000..68665f629 --- /dev/null +++ b/test/regress/regress1/bug590.smt2 @@ -0,0 +1,61 @@ +(set-logic QF_ALL_SUPPORTED) +(set-option :strings-exp true) +(set-option :produce-models true) +(set-info :smt-lib-version 2.0) +(set-info :status unknown) + +(declare-fun text () String) +(declare-fun output () String) + +; html_escape_table = { +; "&": "&", +; '"': """, +; "'": "'", +; ">": ">", +; "<": "<", +; } +(declare-fun html_escape_table () (Array String String)) +(assert (= html_escape_table + (store (store (store (store (store ((as const (Array String String)) "A") + "&" "&") + "\"" """) + "'" "'") + ">" ">") + "<" "<"))) +(declare-fun html_escape_table_keys () (Array Int String)) +(assert (= html_escape_table_keys + (store (store (store (store (store ((as const (Array Int String)) "B") + 0 "&") + 1 "\"") + 2 "'") + 3 ">") + 4 "<"))) + +; charlst = [c for c in text] +(declare-fun charlst () (Array Int String)) +(declare-fun charlstlen () Int) +(assert (= charlstlen (str.len text))) +(assert (forall ((i Int)) + (= (select charlst i) (str.at text i)) +)) + +; charlst2 = [html_escape_table.get(c, c) for c in charlst] +(declare-fun charlst2 () (Array Int String)) +(declare-fun charlstlen2 () Int) +(assert (= charlstlen2 charlstlen)) +(assert (forall ((i Int)) + (or (or (< i 0) (>= i charlstlen2)) + (and (exists ((j Int)) + (= (select html_escape_table_keys j) (select charlst i)) + ) + (= (select charlst2 i) (select html_escape_table (select charlst i))) + ) + (and (not (exists ((j Int)) + (= (select html_escape_table_keys j) (select charlst i)) + )) + (= (select charlst2 i) (select charlst i)) + ) + ) +)) +(check-sat) +(get-value (charlst2)) |