projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a2f099d) | patch
Add regressions for array sequence solver (#7874)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 7 Jan 2022 16:32:34 +0000 (10:32 -0600)
committerGitHub <noreply@github.com>
Fri, 7 Jan 2022 16:32:34 +0000 (16:32 +0000)
commit4351f84f5bde316386aa2226a63bd9bf42659fca
tree211ee6af5129e817c674b7dc03ed969506d04812tree
parenta2f099d72f65bbfe4224bc96ed16c1b423774760commit | diff
Add regressions for array sequence solver (#7874)

This closes the seqArray branch.
15 files changed:
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/seq/array/array1.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/array/array2.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/array/array3.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/array/array4.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/array/distinct-update.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/array/model-dd-1220.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/array/nth-concat.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/array/update-fallback.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/array/update-word-eq.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/rev.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/seqa-model-unsound-dd.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/update-eq-unsat.smt2 [new file with mode: 0644] blob
test/regress/regress1/quantifiers/seqa-unsat-unknown-110921.smt2 [new file with mode: 0644] blob
test/regress/regress1/strings/seq-skeleton-gap.smt2 [new file with mode: 0644] blob