From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 18 Jun 2021 00:49:15 +0000 (-0700)
Subject: Fix build without libpoly (#6759)
X-Git-Tag: cvc5-1.0.0~1592
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=204d645e97bbacd948b5777b704f7b418577610a;p=cvc5.git

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 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)