From 204d645e97bbacd948b5777b704f7b418577610a Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 17 Jun 2021 17:49:15 -0700
Subject: [PATCH] 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.
---
 src/theory/arith/nl/cad/lazard_evaluation.cpp | 4 ++++
 src/theory/arith/nl/cad/lazard_evaluation.h   | 5 ++++-
 test/regress/regress0/nl/issue3003.smt2       | 2 +-
 3 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/theory/arith/nl/cad/lazard_evaluation.cpp b/src/theory/arith/nl/cad/lazard_evaluation.cpp
index 82b127ed0..2fee21cbf 100644
--- 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 0edb12010..3bb971c4c 100644
--- 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 f28a1fd77..3247a941a 100644
--- 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)
-- 
2.30.2