diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-11-24 20:15:00 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-25 04:15:00 +0000 |
| commit | 772d43ea8498e65ef177173266cbfcd741403d40 (patch) | |
| tree | 8850478dd65bb00b2e88e07e144eb889e2b0f2d8 /test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 | |
| parent | 943dfc57d1bbc58046ad10bb4a8a48a8b654aeb5 (diff) | |
Guard regression tests that require libpoly to pass. (#7698)
Regression tests either timeout or return unknown if cvc5 is configured with --no-poly.
Diffstat (limited to 'test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2')
| -rw-r--r-- | test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 index 512c8d2e1..16f24ac0d 100644 --- a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 +++ b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 @@ -1,5 +1,6 @@ ; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/; s/((x (witness ((BOUND_VARIABLE Real)) (.*/SUCCESS/' ; COMMAND-LINE: --produce-models --model-witness-value --no-check-models +; REQUIRES: poly ; EXPECT: sat ; EXPECT: SUCCESS (set-logic QF_NRA) |