From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 5 Aug 2020 02:32:10 +0000 (+0200)
Subject: Add dummy returns if libpoly is unavailable. (#4845)
X-Git-Tag: cvc5-1.0.0~3040
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c324bb21adb44374eb37a0254e31c0a0d0b3ebc7;p=cvc5.git

Add dummy returns if libpoly is unavailable. (#4845)

This PR adds dummy return statements do CadSolver in case libpoly is not available.
---

diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 783fb0187..a2fc1e1f1 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -102,6 +102,7 @@ std::vector<NlLemma> CadSolver::checkFull()
   Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
                "with --poly."
             << std::endl;
+  return {};
 #endif
 }
 
@@ -132,6 +133,7 @@ bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions)
   Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
                "with --poly."
             << std::endl;
+  return false;
 #endif
 }