From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Thu, 31 Oct 2019 21:39:29 +0000 (-0700)
Subject: Fix Unimplemented() macros missed in #3366. (#3424)
X-Git-Tag: cvc5-1.0.0~3867
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e5992fc62ac04a7dff4165c2e54282ac06bd7283;p=cvc5.git

Fix Unimplemented() macros missed in #3366. (#3424)
---

diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index f35c343bd..f824f5075 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -18,6 +18,7 @@
 
 #ifdef CVC4_USE_CADICAL
 
+#include "base/check.h"
 #include "proof/sat_proof.h"
 
 namespace CVC4 {
@@ -116,7 +117,7 @@ SatValue CadicalSolver::solve()
 
 SatValue CadicalSolver::solve(long unsigned int&)
 {
-  Unimplemented("Setting limits for CaDiCaL not supported yet");
+  Unimplemented() << "Setting limits for CaDiCaL not supported yet";
 };
 
 SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 8a70bedce..9893f1d6c 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -18,6 +18,7 @@
 
 #include "prop/cryptominisat.h"
 
+#include "base/check.h"
 #include "proof/clause_id.h"
 #include "proof/sat_proof.h"
 
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index c8a03fab1..c95d6f53d 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -206,7 +206,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       if(t[0].getType().isInteger()) {
         return RewriteResponse(REWRITE_DONE, t[0]);
       }
-      //Unimplemented("TO_INTEGER, nonconstant");
+      //Unimplemented() << "TO_INTEGER, nonconstant";
       //return rewriteToInteger(t);
       return RewriteResponse(REWRITE_DONE, t);
     case kind::IS_INTEGER:
@@ -216,7 +216,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       if(t[0].getType().isInteger()) {
         return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
       }
-      //Unimplemented("IS_INTEGER, nonconstant");
+      //Unimplemented() << "IS_INTEGER, nonconstant";
       //return rewriteIsInteger(t);
       return RewriteResponse(REWRITE_DONE, t);
     case kind::POW:
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index bb1e434f2..98e330df4 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1684,12 +1684,12 @@ void CardinalityExtension::preRegisterTerm(TNode n)
           Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier";
           Debug("uf-ss-na") << " (" << f << ")";
           Debug("uf-ss-na") << std::endl;
-          Unimplemented("Cannot perform finite model finding on arithmetic quantifier");
+          Unimplemented() << "Cannot perform finite model finding on arithmetic quantifier";
         }else if( tn.isDatatype() ){
           Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier";
           Debug("uf-ss-na") << " (" << f << ")";
           Debug("uf-ss-na") << std::endl;
-          Unimplemented("Cannot perform finite model finding on datatype quantifier");
+          Unimplemented() << "Cannot perform finite model finding on datatype quantifier";
         }
         */
       }