Fix build without libpoly (#6759)

Commit f10087c3b347da6ef625a2ad92846551ad324d73 added new files that do
not compile without libpoly. This commit excludes those files when
building without libpoly. It also updates one of the regressions to
ignore a warning about approximate values in the model.

diff --git a/src/theory/arith/nl/cad/lazard_evaluation.cpp b/src/theory/arith/nl/cad/lazard_evaluation.cpp
index 82b127ed0f3726b9f5ba195a9de5b6bb203797a7..2fee21cbf525948748baa63d2cc0896d8af288f8 100644 (file)
--- a/src/theory/arith/nl/cad/lazard_evaluation.cpp
+++ b/src/theory/arith/nl/cad/lazard_evaluation.cpp
@@ -1,5 +1,7 @@
 #include "theory/arith/nl/cad/lazard_evaluation.h"
 
+#ifdef CVC5_POLY_IMP
+
 #include "base/check.h"
 #include "base/output.h"
 
@@ -44,3 +46,5 @@ std::vector<poly::Interval> LazardEvaluation::infeasibleRegions(
 }
 
 }  // namespace cvc5::theory::arith::nl::cad
+
+#endif

diff --git a/src/theory/arith/nl/cad/lazard_evaluation.h b/src/theory/arith/nl/cad/lazard_evaluation.h
index 0edb120105a37c45333718403e7003f3fefd91d8..3bb971c4c57aab455d5656dc8a9071eecf0e6ed9 100644 (file)
--- a/src/theory/arith/nl/cad/lazard_evaluation.h
+++ b/src/theory/arith/nl/cad/lazard_evaluation.h
@@ -19,6 +19,8 @@
 #ifndef CVC5__THEORY__ARITH__NL__CAD__LAZARD_EVALUATION_H
 #define CVC5__THEORY__ARITH__NL__CAD__LAZARD_EVALUATION_H
 
+#ifdef CVC5_POLY_IMP
+
 #include <poly/polyxx.h>
 
 #include <memory>
@@ -106,4 +108,5 @@ class LazardEvaluation
 
 }  // namespace cvc5::theory::arith::nl::cad
 
-#endif
\ No newline at end of file
+#endif
+#endif

diff --git a/test/regress/regress0/nl/issue3003.smt2 b/test/regress/regress0/nl/issue3003.smt2
index f28a1fd7745365b07ab9d24a796337a5d1ad92cc..3247a941aa8f1a7ebdff9e6a9e557e5fd18d408a 100644 (file)
--- a/test/regress/regress0/nl/issue3003.smt2
+++ b/test/regress/regress0/nl/issue3003.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext=none
+; COMMAND-LINE: --nl-ext=none --no-check-models
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :status sat)