From c324bb21adb44374eb37a0254e31c0a0d0b3ebc7 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 5 Aug 2020 04:32:10 +0200 Subject: [PATCH] Add dummy returns if libpoly is unavailable. (#4845) This PR adds dummy return statements do CadSolver in case libpoly is not available. --- src/theory/arith/nl/cad_solver.cpp | 2 ++ 1 file changed, 2 insertions(+) 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 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& assertions) Warning() << "Tried to use CadSolver but libpoly is not available. Compile " "with --poly." << std::endl; + return false; #endif } -- 2.30.2