projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 60c9b49)
Add requires libpoly to regression (#7467)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 22 Oct 2021 23:28:09 +0000 (18:28 -0500)
committerGitHub <noreply@github.com>
Fri, 22 Oct 2021 23:28:09 +0000 (23:28 +0000)
Required to avoid timeout in non-libpoly builds.

FYI @dddejan .

test/regress/regress1/nl/approx-sqrt-unsat.smt2 patch | blob | history

diff --git a/test/regress/regress1/nl/approx-sqrt-unsat.smt2 b/test/regress/regress1/nl/approx-sqrt-unsat.smt2
index cda24d09871607c2e3ea89bfbf946aee4532429f..774dbffcb487180f600d1182cd27ca1dd4414bdc 100644 (file)
--- a/test/regress/regress1/nl/approx-sqrt-unsat.smt2
+++ b/test/regress/regress1/nl/approx-sqrt-unsat.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: poly
 ; COMMAND-LINE: --nl-ext-tplanes --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_NRA)