diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 10:18:16 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 10:18:16 -0600 |
| commit | 0e956da9b32ce8a8fcf20ec65e5a2820b4e31324 (patch) | |
| tree | 97d5d40da911ce9bd5f458e301b381986e7cba40 /test | |
| parent | 4db65cbaf87f87dba3682e88563f5a923f265152 (diff) | |
Fix nf exp tracking for non-linear string equalities, fixes bug 768.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/strings/bug768.smt2 | 10 |
2 files changed, 12 insertions, 1 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 70fec7b82..a77c2bd6c 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -84,7 +84,8 @@ TESTS = \ cmu-substr-rw.smt2 \ gm-inc-071516-2.smt2 \ cmu-inc-nlpp-071516.smt2 \ - strings-index-empty.smt2 + strings-index-empty.smt2 \ + bug768.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/bug768.smt2 b/test/regress/regress0/strings/bug768.smt2 new file mode 100644 index 000000000..be3f24200 --- /dev/null +++ b/test/regress/regress0/strings/bug768.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_S) +(set-info :status sat) +(declare-fun f0 () String) +(declare-fun c0 () String) +(declare-fun f1 () String) +(declare-fun f2 () String) + +(assert (= (str.++ f0 f1 f0 c0 f1 c0 f2 f2) "f(,f(c,c))")) + +(check-sat) |