12 files changed, 26 insertions, 14 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 44768009e..611689c2b 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -113,15 +113,12 @@ SatLiteral TseitinCnfStream::handleAtom(TNode node) {
   bool theoryLiteral = node.getKind() != kind::VARIABLE;
   SatLiteral lit = newLiteral(node, theoryLiteral);
 
-  switch(node.getKind()) {
-  case TRUE:
-    assertClause(lit);
-    break;
-  case FALSE:
-    assertClause(~lit);
-    break;
-  default:
-    break;
+  if(node.getKind() == kind::CONST_BOOLEAN) {
+    if(node.getConst<bool>()) {
+      assertClause(lit);
+    } else {
+      assertClause(~lit);
+    }
   }
 
   return lit;
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 131999e38..bf2018338 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -17,16 +17,16 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__PROP__MINISAT__SOLVER_H
 #define __CVC4__PROP__MINISAT__SOLVER_H
 
-#include "cvc4_private.h"
 #include "context/context.h"
 
 #include <cstdio>
 #include <cassert>
 
-#include "cvc4_config.h"
 #include "../mtl/Vec.h"
 #include "../mtl/Heap.h"
 #include "../mtl/Alg.h"
diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
index 0fe6d84c7..e636f2b87 100644
--- a/src/prop/minisat/mtl/Alg.h
+++ b/src/prop/minisat/mtl/Alg.h
@@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef CVC4_MiniSat_Alg_h
 #define CVC4_MiniSat_Alg_h
 
diff --git a/src/prop/minisat/mtl/BasicHeap.h b/src/prop/minisat/mtl/BasicHeap.h
index 39d825411..cb6a7cbd8 100644
--- a/src/prop/minisat/mtl/BasicHeap.h
+++ b/src/prop/minisat/mtl/BasicHeap.h
@@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef CVC4_MiniSat_BasicHeap_h
 #define CVC4_MiniSat_BasicHeap_h
 
diff --git a/src/prop/minisat/mtl/BoxedVec.h b/src/prop/minisat/mtl/BoxedVec.h
index 05b801004..7cf5ba14f 100644
--- a/src/prop/minisat/mtl/BoxedVec.h
+++ b/src/prop/minisat/mtl/BoxedVec.h
@@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef CVC4_MiniSat_BoxedVec_h
 #define CVC4_MiniSat_BoxedVec_h
 
diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
index 0c2019b65..20d379b1d 100644
--- a/src/prop/minisat/mtl/Heap.h
+++ b/src/prop/minisat/mtl/Heap.h
@@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef CVC4_MiniSat_Heap_h
 #define CVC4_MiniSat_Heap_h
 
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index 9168dde0e..715b84da4 100644
--- a/src/prop/minisat/mtl/Map.h
+++ b/src/prop/minisat/mtl/Map.h
@@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef CVC4_MiniSat_Map_h
 #define CVC4_MiniSat_Map_h
 
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
index e02ac7222..291a1f2e3 100644
--- a/src/prop/minisat/mtl/Queue.h
+++ b/src/prop/minisat/mtl/Queue.h
@@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef CVC4_MiniSat_Queue_h
 #define CVC4_MiniSat_Queue_h
 
diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h
index 2b9d5bb15..19e89803b 100644
--- a/src/prop/minisat/mtl/Sort.h
+++ b/src/prop/minisat/mtl/Sort.h
@@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef CVC4_MiniSat_Sort_h
 #define CVC4_MiniSat_Sort_h
 
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index fae1d0c5d..364991aa9 100644
--- a/src/prop/minisat/mtl/Vec.h
+++ b/src/prop/minisat/mtl/Vec.h
@@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
+#include "cvc4_private.h"
+
 #ifndef CVC4_MiniSat_Vec_h
 #define CVC4_MiniSat_Vec_h
 
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index d699153b2..36f6cb0cb 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -19,7 +19,6 @@
 #ifndef __CVC4__PROP_ENGINE_H
 #define __CVC4__PROP_ENGINE_H
 
-#include "cvc4_config.h"
 #include "expr/node.h"
 #include "util/result.h"
 #include "util/options.h"
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 93e95eedf..207ed90fd 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -13,11 +13,11 @@
  ** SAT Solver.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__PROP__SAT_H
 #define __CVC4__PROP__SAT_H
 
-#include "cvc4_private.h"
-
 #define __CVC4_USE_MINISAT
 
 #ifdef __CVC4_USE_MINISAT