diff --git a/cvc4-flags.patch b/cvc4-flags.patch
index 4793ace..c26da0b 100644
--- a/cvc4-flags.patch
+++ b/cvc4-flags.patch
@@ -45,59 +45,6 @@
  
  CFLAGS    += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
  LFLAGS    += -lz
---- src/prop/cryptominisat.cpp.orig	2019-04-09 10:14:31.000000000 -0600
-+++ src/prop/cryptominisat.cpp	2020-04-26 14:04:26.086833393 -0600
-@@ -68,15 +68,8 @@ CryptoMinisatSolver::CryptoMinisatSolver
-       d_okay(true),
-       d_statistics(registry, name)
- {
--  d_true = newVar();
--  d_false = newVar();
--
--  std::vector<CMSat::Lit> clause(1);
--  clause[0] = CMSat::Lit(d_true, false);
--  d_solver->add_clause(clause);
--  
--  clause[0] = CMSat::Lit(d_false, true);
--  d_solver->add_clause(clause);
-+  d_true = undefSatVariable;
-+  d_false = undefSatVariable;
- }
- 
- 
-@@ -154,10 +147,32 @@ SatVariable  CryptoMinisatSolver::newVar
- }
- 
- SatVariable CryptoMinisatSolver::trueVar() {
-+  if (d_true == undefSatVariable) {
-+    d_true = newVar();
-+    d_false = newVar();
-+
-+    std::vector<CMSat::Lit> clause(1);
-+    clause[0] = CMSat::Lit(d_true, false);
-+    d_solver->add_clause(clause);
-+
-+    clause[0] = CMSat::Lit(d_false, true);
-+    d_solver->add_clause(clause);
-+  }
-   return d_true;
- }
- 
- SatVariable CryptoMinisatSolver::falseVar() {
-+  if (d_true == undefSatVariable) {
-+    d_true = newVar();
-+    d_false = newVar();
-+
-+    std::vector<CMSat::Lit> clause(1);
-+    clause[0] = CMSat::Lit(d_true, false);
-+    d_solver->add_clause(clause);
-+
-+    clause[0] = CMSat::Lit(d_false, true);
-+    d_solver->add_clause(clause);
-+  }
-   return d_false;
- }
- 
 --- src/prop/minisat/mtl/template.mk.orig	2019-04-09 10:14:31.000000000 -0600
 +++ src/prop/minisat/mtl/template.mk	2019-04-17 11:22:15.879002442 -0600
 @@ -22,7 +22,7 @@ CXX       ?= g++