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

diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index f35c343bd996d2fa5cc66b9183af2da6f8b879d4..f824f50751883b610e2f5cebc8c4920d22d63fcc 100644 (file)
--- 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 8a70bedce010f1e948e69e80da7a3701d60b5645..9893f1d6c07b0c0223fcf2079e6d5260b9d1920a 100644 (file)
--- 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 c8a03fab1bc94761bcad8abeff337b72c4272696..c95d6f53dcde1d72836f652e1c4aec912dc9d55d 100644 (file)
--- 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 bb1e434f21da5bef934117a19450ce56f4ed99d5..98e330df48f42eae4d3cee6a29f7f0db768a8b41 100644 (file)
--- 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";
         }
         */
       }