projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 943dfc5) | patch
Guard regression tests that require libpoly to pass. (#7698)
authorMathias Preiner <mathias.preiner@gmail.com>
Thu, 25 Nov 2021 04:15:00 +0000 (20:15 -0800)
committerGitHub <noreply@github.com>
Thu, 25 Nov 2021 04:15:00 +0000 (04:15 +0000)
commit772d43ea8498e65ef177173266cbfcd741403d40
tree8850478dd65bb00b2e88e07e144eb889e2b0f2d8tree
parent943dfc57d1bbc58046ad10bb4a8a48a8b654aeb5commit | diff
Guard regression tests that require libpoly to pass. (#7698)

Regression tests either timeout or return unknown if cvc5 is configured with --no-poly.
test/regress/regress0/nl/issue3003.smt2 diff | blob | history
test/regress/regress0/nl/issue3411.smt2 diff | blob | history
test/regress/regress0/nl/issue3652.smt2 diff | blob | history
test/regress/regress0/nl/issue3719.smt2 diff | blob | history
test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 diff | blob | history
test/regress/regress0/nl/sqrt2-value.smt2 diff | blob | history
test/regress/regress1/nl/approx-sqrt.smt2 diff | blob | history
test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 diff | blob | history
test/regress/regress1/nl/solve-eq-small-qf-nra.smt2 diff | blob | history
test/regress/regress1/quantifiers/issue6607-witness-te.smt2 diff | blob | history
test/regress/regress1/sqrt2-sort-inf-unk.smt2 diff | blob | history