From a5c952d63bca9f94d3886db4d9c09d08d7a23033 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 7 Feb 2018 10:19:04 -0800
Subject: Adds a new CHECK macro that abort()s on failure. (#1532)

---
 src/theory/bv/aig_bitblaster.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'src/theory')

diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 5459340f6..010eaf4e5 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -15,7 +15,10 @@
  **/
 
 #include "bitblaster_template.h"
+
 #include "cvc4_private.h"
+
+#include "base/cvc4_check.h"
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
@@ -155,8 +158,7 @@ AigBitblaster::AigBitblaster()
     d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(),
                                                               "AigBitblaster");
     break;
-  default:
-    Unreachable("Unknown SAT solver type");
+  default: CVC4_FATAL() << "Unknown SAT solver type";
   }
 }
 
-- 
cgit v1.2.3