--- src/prop/cryptominisat.cpp.orig	2020-06-19 10:59:27.000000000 -0600
+++ src/prop/cryptominisat.cpp	2020-06-21 11:51:21.496211208 -0600
@@ -73,15 +73,8 @@ CryptoMinisatSolver::CryptoMinisatSolver
 
 void CryptoMinisatSolver::init()
 {
-  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;
 }
 
 CryptoMinisatSolver::~CryptoMinisatSolver() {}
@@ -158,10 +151,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;
 }