diff --git a/CMakeLists.txt b/CMakeLists.txt
index bc86e39eea8..d8f25fe698a 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -62,7 +62,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
     set(CMAKE_CXX_FLAGS_RELEASE "-O2")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g")
     #   Enable lots of warnings
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wswitch-enum")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Wno-deprecated-declarations -Wswitch-enum")
 elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     # This would be the place to enable warnings for Windows builds, although
     # config.inc doesn't seem to do that currently
diff --git a/src/Makefile b/src/Makefile
index 81ca5124eac..e65bda5da04 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -119,19 +119,18 @@ DOWNLOADER = curl -L --remote-name
 TAR = tar
 
 minisat2-download:
-	@echo "Downloading Minisat 2.2.1"
+	@echo "Downloading MergeSat (replacing Minisat 2.2.1)"
 	@for i in $$(seq 1 3) ; do \
 	  $(DOWNLOADER) \
-	    http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz && \
+	    https://github.com/conp-solutions/mergesat/archive/refs/tags/v3.0.tar.gz && \
 	    exit 0 ; \
-		$(RM) minisat2_2.2.1.orig.tar.gz ; \
+		$(RM) v3.0.tar.gz ; \
 	  if [ $$i -lt 3 ] ; then echo "Re-trying in 10 seconds" 1>&2 ; sleep 10 ; fi ; \
 	done ; exit 1
-	@$(TAR) xfz minisat2_2.2.1.orig.tar.gz
+	@$(TAR) xfz v3.0.tar.gz # will create mergesat-3.0
 	@rm -Rf ../minisat-2.2.1
-	@mv minisat2-2.2.1 ../minisat-2.2.1
-	@(cd ../minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch)
-	@rm minisat2_2.2.1.orig.tar.gz
+	@mv mergesat-3.0 ../minisat-2.2.1
+	@rm v3.0.tar.gz
 
 cudd-download:
 	@echo "Downloading Cudd 3.0.0"
diff --git a/src/config.inc b/src/config.inc
index b679d7cebec..25b57e095dd 100644
--- a/src/config.inc
+++ b/src/config.inc
@@ -5,7 +5,7 @@ BUILD_ENV = AUTO
 ifeq ($(BUILD_ENV),MSVC)
   #CXXFLAGS += /Wall /WX
 else
-  CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations -Wswitch-enum
+  CXXFLAGS += -Wall -pedantic -Wno-deprecated-declarations -Wswitch-enum
 endif
 
 ifeq ($(CPROVER_WITH_PROFILING),1)
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index c8569eb084f..af12d515fa2 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -17,7 +17,7 @@ endif
 ifneq ($(MINISAT2),)
   MINISAT2_SRC=sat/satcheck_minisat2.cpp
   MINISAT2_INCLUDE=-I $(MINISAT2)
-  MINISAT2_LIB=$(MINISAT2)/minisat/simp/SimpSolver$(OBJEXT) $(MINISAT2)/minisat/core/Solver$(OBJEXT)
+  MINISAT2_LIB=$(MINISAT2)/minisat/simp/SimpSolver$(OBJEXT) $(MINISAT2)/minisat/core/Solver$(OBJEXT) $(MINISAT2)/minisat/utils/ccnr$(OBJEXT) $(MINISAT2)/minisat/utils/Options$(OBJEXT) $(MINISAT2)/minisat/utils/System$(OBJEXT)
   CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
   CLEANFILES += $(MINISAT2_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(MINISAT2_LIB))
 endif
@@ -201,6 +201,15 @@ ifeq ($(BUILD_ENV_),MSVC)
 sat/satcheck_minisat2$(OBJEXT): sat/satcheck_minisat2.cpp
 	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
 
+$(MINISAT2)/minisat/utils/ccnr$(OBJEXT): $(MINISAT2)/minisat/utils/ccnr.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MINISAT2)/minisat/utils/Options$(OBJEXT): $(MINISAT2)/minisat/utils/Options.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MINISAT2)/minisat/utils/System$(OBJEXT): $(MINISAT2)/minisat/utils/System.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
 $(MINISAT2)/minisat/simp/SimpSolver$(OBJEXT): $(MINISAT2)/minisat/simp/SimpSolver.cc
 	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
 
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index f42b029aa11..0c2f483b918 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -77,7 +77,7 @@ void satcheck_minisat2_baset<T>::set_polarity(literalt a, bool value)
   try
   {
     add_variables();
-    solver->setPolarity(a.var_no(), value ? l_True : l_False);
+    solver->setPolarity(a.var_no(), value); // ? l_True : l_False);
   }
   catch(Minisat::OutOfMemoryException)
   {