diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2014-10-21 13:03:40 -0700 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2014-10-21 13:03:40 -0700 |
commit | ff3efb7f258c04a3371e28da3558451a4c81f000 (patch) | |
tree | 4f3216112abc4b7bd61946320a9f0dc3369afc2d /test/regress/regress0 | |
parent | bb41d77bae405cad83ee26b85cda7ad84e0abb14 (diff) |
Fixed bug 590, added regression test
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/bug590.smt2 | 60 | ||||
-rw-r--r-- | test/regress/regress0/bug590.smt2.expect | 2 |
3 files changed, 64 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index e7b8e3b73..11d0647bc 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -165,7 +165,8 @@ BUG_TESTS = \ bug576a.smt2 \ bug578.smt2 \ bug585.cvc \ - bug586.cvc + bug586.cvc \ + bug590.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug590.smt2 b/test/regress/regress0/bug590.smt2 new file mode 100644 index 000000000..d5bd7fd56 --- /dev/null +++ b/test/regress/regress0/bug590.smt2 @@ -0,0 +1,60 @@ +(set-logic QF_ALL_SUPPORTED) +(set-option :strings-exp true) +(set-option :produce-models true) +(set-info :status sat) + +(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)) diff --git a/test/regress/regress0/bug590.smt2.expect b/test/regress/regress0/bug590.smt2.expect new file mode 100644 index 000000000..67f25bb72 --- /dev/null +++ b/test/regress/regress0/bug590.smt2.expect @@ -0,0 +1,2 @@ +% EXPECT: sat +% EXPECT: ((charlst2 (store ((as const (Array Int String)) "C") 0 "<"))) |