Replaced ezDefaultSAT with ezSatPtr

3 files changed, 74 insertions, 73 deletions

diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
index 62534ec0b..01d0e031c 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.cc
@@ -143,16 +143,16 @@ struct VlogHammerReporter
 	{
 		log("Verifying SAT model (%s)..\n", model_undef ? "with undef" : "without undef");
 
-		ezDefaultSAT ez;
+		ezSatPtr ez;
 		SigMap sigmap(module);
-		SatGen satgen(&ez, &sigmap);
+		SatGen satgen(ez.get(), &sigmap);
 		satgen.model_undef = model_undef;
 
 		for (auto &c : module->cells_)
 			if (!satgen.importCell(c.second))
 				log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
 
-		ez.assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals));
+		ez->assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals));
 
 		std::vector<int> y_vec = satgen.importDefSigSpec(module->wires_.at("\\y"));
 		std::vector<bool> y_values;
@@ -163,9 +163,9 @@ struct VlogHammerReporter
 		}
 
 		log("  Created SAT problem with %d variables and %d clauses.\n",
-				ez.numCnfVariables(), ez.numCnfClauses());
+				ez->numCnfVariables(), ez->numCnfClauses());
 
-		if (!ez.solve(y_vec, y_values))
+		if (!ez->solve(y_vec, y_values))
 			log_error("Failed to find solution to SAT problem.\n");
 
 		for (int i = 0; i < expected_y.size(); i++) {
@@ -204,7 +204,7 @@ struct VlogHammerReporter
 				if (y_undef.at(i))
 				{
 					log("    Toggling undef bit %d to test undef gating.\n", i);
-					if (!ez.solve(y_vec, y_values, ez.IFF(y_vec.at(i), y_values.at(i) ? ez.CONST_FALSE : ez.CONST_TRUE)))
+					if (!ez->solve(y_vec, y_values, ez->IFF(y_vec.at(i), y_values.at(i) ? ez->CONST_FALSE : ez->CONST_TRUE)))
 						log_error("Failed to find solution with toggled bit!\n");
 
 					cmp_vars.push_back(y_vec.at(expected_y.size() + i));
@@ -220,15 +220,15 @@ struct VlogHammerReporter
 				}
 
 			log("    Testing if SAT solution is unique.\n");
-			ez.assume(ez.vec_ne(cmp_vars, ez.vec_const(cmp_vals)));
-			if (ez.solve(y_vec, y_values))
+			ez->assume(ez->vec_ne(cmp_vars, ez->vec_const(cmp_vals)));
+			if (ez->solve(y_vec, y_values))
 				log_error("Found two distinct solutions to SAT problem.\n");
 		}
 		else
 		{
 			log("    Testing if SAT solution is unique.\n");
-			ez.assume(ez.vec_ne(y_vec, ez.vec_const(y_values)));
-			if (ez.solve(y_vec, y_values))
+			ez->assume(ez->vec_ne(y_vec, ez->vec_const(y_values)));
+			if (ez->solve(y_vec, y_values))
 				log_error("Found two distinct solutions to SAT problem.\n");
 		}
 
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index fbca35861..8a5301ec3 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -73,7 +73,7 @@ struct FindReducedInputs
 	SigMap &sigmap;
 	drivers_t &drivers;
 
-	ezDefaultSAT ez;
+	ezSatPtr ez;
 	std::set<RTLIL::Cell*> ez_cells;
 	SatGen satgen;
 
@@ -81,7 +81,7 @@ struct FindReducedInputs
 	std::vector<int> sat_pi_uniq_bitvec;
 
 	FindReducedInputs(SigMap &sigmap, drivers_t &drivers) :
-			sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap)
+			sigmap(sigmap), drivers(drivers), satgen(ez.get(), &sigmap)
 	{
 		satgen.model_undef = true;
 	}
@@ -104,30 +104,30 @@ struct FindReducedInputs
 
 		satgen.setContext(&sigmap, "A");
 		int sat_a = satgen.importSigSpec(bit).front();
-		ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front()));
+		ez->assume(ez->NOT(satgen.importUndefSigSpec(bit).front()));
 
 		satgen.setContext(&sigmap, "B");
 		int sat_b = satgen.importSigSpec(bit).front();
-		ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front()));
+		ez->assume(ez->NOT(satgen.importUndefSigSpec(bit).front()));
 
 		int idx = sat_pi.size();
 		size_t idx_bits = get_bits(idx);
 
 		if (sat_pi_uniq_bitvec.size() != idx_bits) {
-			sat_pi_uniq_bitvec.push_back(ez.frozen_literal(stringf("uniq_%d", int(idx_bits)-1)));
+			sat_pi_uniq_bitvec.push_back(ez->frozen_literal(stringf("uniq_%d", int(idx_bits)-1)));
 			for (auto &it : sat_pi)
-				ez.assume(ez.OR(ez.NOT(it.second), ez.NOT(sat_pi_uniq_bitvec.back())));
+				ez->assume(ez->OR(ez->NOT(it.second), ez->NOT(sat_pi_uniq_bitvec.back())));
 		}
 		log_assert(sat_pi_uniq_bitvec.size() == idx_bits);
 
-		sat_pi[bit] = ez.frozen_literal(stringf("p, falsei_%s", log_signal(bit)));
-		ez.assume(ez.IFF(ez.XOR(sat_a, sat_b), sat_pi[bit]));
+		sat_pi[bit] = ez->frozen_literal(stringf("p, falsei_%s", log_signal(bit)));
+		ez->assume(ez->IFF(ez->XOR(sat_a, sat_b), sat_pi[bit]));
 
 		for (size_t i = 0; i < idx_bits; i++)
 			if ((idx & (1 << i)) == 0)
-				ez.assume(ez.OR(ez.NOT(sat_pi[bit]), ez.NOT(sat_pi_uniq_bitvec[i])));
+				ez->assume(ez->OR(ez->NOT(sat_pi[bit]), ez->NOT(sat_pi_uniq_bitvec[i])));
 			else
-				ez.assume(ez.OR(ez.NOT(sat_pi[bit]), sat_pi_uniq_bitvec[i]));
+				ez->assume(ez->OR(ez->NOT(sat_pi[bit]), sat_pi_uniq_bitvec[i]));
 	}
 
 	void register_cone_worker(std::set<RTLIL::SigBit> &pi, std::set<RTLIL::SigBit> &sigdone, RTLIL::SigBit out)
@@ -201,7 +201,7 @@ struct FindReducedInputs
 					model_expr.push_back(sat_pi.at(pi[i]));
 				}
 
-			if (!ez.solve(model_expr, model, ez.expression(ezSAT::OpOr, model_expr), ez.XOR(output_a, output_b), ez.NOT(output_undef_a), ez.NOT(output_undef_b)))
+			if (!ez->solve(model_expr, model, ez->expression(ezSAT::OpOr, model_expr), ez->XOR(output_a, output_b), ez->NOT(output_undef_a), ez->NOT(output_undef_b)))
 				break;
 
 			int found_count = 0;
@@ -230,7 +230,7 @@ struct PerformReduction
 	drivers_t &drivers;
 	std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs;
 
-	ezDefaultSAT ez;
+	ezSatPtr ez;
 	SatGen satgen;
 
 	std::vector<int> sat_pi, sat_out, sat_def;
@@ -260,7 +260,7 @@ struct PerformReduction
 		} else {
 			pi_bits.push_back(out);
 			sat_pi.push_back(satgen.importSigSpec(out).front());
-			ez.assume(ez.NOT(satgen.importUndefSigSpec(out).front()));
+			ez->assume(ez->NOT(satgen.importUndefSigSpec(out).front()));
 			sigdepth[out] = 0;
 		}
 
@@ -268,7 +268,7 @@ struct PerformReduction
 	}
 
 	PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs, std::vector<RTLIL::SigBit> &bits, int cone_size) :
-			sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(&ez, &sigmap), out_bits(bits), cone_size(cone_size)
+			sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(ez.get(), &sigmap), out_bits(bits), cone_size(cone_size)
 	{
 		satgen.model_undef = true;
 
@@ -278,15 +278,15 @@ struct PerformReduction
 		for (auto &bit : bits) {
 			out_depth.push_back(register_cone_worker(celldone, sigdepth, bit));
 			sat_out.push_back(satgen.importSigSpec(bit).front());
-			sat_def.push_back(ez.NOT(satgen.importUndefSigSpec(bit).front()));
+			sat_def.push_back(ez->NOT(satgen.importUndefSigSpec(bit).front()));
 		}
 
 		if (inv_mode && cone_size > 0) {
-			if (!ez.solve(sat_out, out_inverted, ez.expression(ezSAT::OpAnd, sat_def)))
+			if (!ez->solve(sat_out, out_inverted, ez->expression(ezSAT::OpAnd, sat_def)))
 				log_error("Solving for initial model failed!\n");
 			for (size_t i = 0; i < sat_out.size(); i++)
 				if (out_inverted.at(i))
-					sat_out[i] = ez.NOT(sat_out[i]);
+					sat_out[i] = ez->NOT(sat_out[i]);
 		} else
 			out_inverted = std::vector<bool>(sat_out.size(), false);
 	}
@@ -296,8 +296,8 @@ struct PerformReduction
 		if (verbose_level == 1)
 			log("    Finding const value for %s.\n", log_signal(out_bits[idx]));
 
-		bool can_be_set = ez.solve(ez.AND(sat_out[idx], sat_def[idx]));
-		bool can_be_clr = ez.solve(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
+		bool can_be_set = ez->solve(ez->AND(sat_out[idx], sat_def[idx]));
+		bool can_be_clr = ez->solve(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx]));
 		log_assert(!can_be_set || !can_be_clr);
 
 		RTLIL::SigBit value(RTLIL::State::Sx);
@@ -355,8 +355,8 @@ struct PerformReduction
 
 		std::vector<int> sat_set_list, sat_clr_list;
 		for (int idx : bucket) {
-			sat_set_list.push_back(ez.AND(sat_out[idx], sat_def[idx]));
-			sat_clr_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
+			sat_set_list.push_back(ez->AND(sat_out[idx], sat_def[idx]));
+			sat_clr_list.push_back(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx]));
 		}
 
 		std::vector<int> modelVars = sat_out;
@@ -366,7 +366,7 @@ struct PerformReduction
 		if (verbose_level >= 2)
 			modelVars.insert(modelVars.end(), sat_pi.begin(), sat_pi.end());
 
-		if (ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_set_list), ez.expression(ezSAT::OpOr, sat_clr_list)))
+		if (ez->solve(modelVars, model, ez->expression(ezSAT::OpOr, sat_set_list), ez->expression(ezSAT::OpOr, sat_clr_list)))
 		{
 			int iter_count = 1;
 
@@ -379,13 +379,13 @@ struct PerformReduction
 
 				for (int idx : bucket)
 					if (!model[sat_out.size() + idx]) {
-						sat_set_list.push_back(ez.AND(sat_out[idx], sat_def[idx]));
-						sat_clr_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
+						sat_set_list.push_back(ez->AND(sat_out[idx], sat_def[idx]));
+						sat_clr_list.push_back(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx]));
 					} else {
 						sat_def_list.push_back(sat_def[idx]);
 					}
 
-				if (!ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_set_list), ez.expression(ezSAT::OpOr, sat_clr_list), ez.expression(ezSAT::OpAnd, sat_def_list)))
+				if (!ez->solve(modelVars, model, ez->expression(ezSAT::OpOr, sat_set_list), ez->expression(ezSAT::OpOr, sat_clr_list), ez->expression(ezSAT::OpAnd, sat_def_list)))
 					break;
 				iter_count++;
 			}
@@ -431,7 +431,7 @@ struct PerformReduction
 				for (int idx2 : bucket)
 					if (idx != idx2)
 						sat_def_list.push_back(sat_def[idx2]);
-				if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list)))
+				if (ez->solve(ez->NOT(sat_def[idx]), ez->expression(ezSAT::OpOr, sat_def_list)))
 					undef_slaves.push_back(idx);
 			}
 
@@ -505,7 +505,7 @@ struct PerformReduction
 				for (int idx2 : r)
 					if (idx != idx2)
 						sat_def_list.push_back(sat_def[idx2]);
-				if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list)))
+				if (ez->solve(ez->NOT(sat_def[idx]), ez->expression(ezSAT::OpOr, sat_def_list)))
 					undef_slaves.push_back(idx);
 			}
 
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index b9535f49d..ad680b6a2 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -41,9 +41,10 @@ struct SatHelper
 	RTLIL::Design *design;
 	RTLIL::Module *module;
 
-	ezDefaultSAT ez;
 	SigMap sigmap;
 	CellTypes ct;
+
+	ezSatPtr ez;
 	SatGen satgen;
 
 	// additional constraints
@@ -65,7 +66,7 @@ struct SatHelper
 	bool gotTimeout;
 
 	SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
-		design(design), module(module), sigmap(module), ct(design), satgen(&ez, &sigmap)
+		design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap)
 	{
 		this->enable_undef = enable_undef;
 		satgen.model_undef = enable_undef;
@@ -155,7 +156,7 @@ struct SatHelper
 		if (set_init_def) {
 			RTLIL::SigSpec rem = satgen.initial_state.export_all();
 			std::vector<int> undef_rem = satgen.importUndefSigSpec(rem, 1);
-			ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_rem)));
+			ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_rem)));
 		}
 
 		if (set_init_undef) {
@@ -179,7 +180,7 @@ struct SatHelper
 
 		log("Final constraint equation: %s = %s\n\n", log_signal(big_lhs), log_signal(big_rhs));
 		check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
-		ez.assume(satgen.signals_eq(big_lhs, big_rhs, 1));
+		ez->assume(satgen.signals_eq(big_lhs, big_rhs, 1));
 	}
 
 	void setup(int timestep = -1)
@@ -250,7 +251,7 @@ struct SatHelper
 
 		log("Final constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
 		check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
-		ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
+		ez->assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
 
 		// 0 = sets_def
 		// 1 = sets_any_undef
@@ -310,11 +311,11 @@ struct SatHelper
 			log("Import %s constraint for this timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
 			std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
 			if (t == 0)
-				ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig)));
+				ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_sig)));
 			if (t == 1)
-				ez.assume(ez.expression(ezSAT::OpOr, undef_sig));
+				ez->assume(ez->expression(ezSAT::OpOr, undef_sig));
 			if (t == 2)
-				ez.assume(ez.expression(ezSAT::OpAnd, undef_sig));
+				ez->assume(ez->expression(ezSAT::OpAnd, undef_sig));
 		}
 
 		int import_cell_counter = 0;
@@ -401,7 +402,7 @@ struct SatHelper
 			std::vector<int> undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep);
 
 			for (size_t i = 0; i < value_lhs.size(); i++)
-				prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i))))));
+				prove_bits.push_back(ez->OR(undef_lhs.at(i), ez->AND(ez->NOT(undef_rhs.at(i)), ez->NOT(ez->XOR(value_lhs.at(i), value_rhs.at(i))))));
 		}
 
 		if (prove_asserts) {
@@ -412,22 +413,22 @@ struct SatHelper
 			prove_bits.push_back(satgen.importAsserts(timestep));
 		}
 
-		return ez.expression(ezSAT::OpAnd, prove_bits);
+		return ez->expression(ezSAT::OpAnd, prove_bits);
 	}
 
 	void force_unique_state(int timestep_from, int timestep_to)
 	{
 		RTLIL::SigSpec state_signals = satgen.initial_state.export_all();
 		for (int i = timestep_from; i < timestep_to; i++)
-			ez.assume(ez.NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to)));
+			ez->assume(ez->NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to)));
 	}
 
 	bool solve(const std::vector<int> &assumptions)
 	{
 		log_assert(gotTimeout == false);
-		ez.setSolverTimeout(timeout);
-		bool success = ez.solve(modelExpressions, modelValues, assumptions);
-		if (ez.getSolverTimoutStatus())
+		ez->setSolverTimeout(timeout);
+		bool success = ez->solve(modelExpressions, modelValues, assumptions);
+		if (ez->getSolverTimoutStatus())
 			gotTimeout = true;
 		return success;
 	}
@@ -435,9 +436,9 @@ struct SatHelper
 	bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0)
 	{
 		log_assert(gotTimeout == false);
-		ez.setSolverTimeout(timeout);
-		bool success = ez.solve(modelExpressions, modelValues, a, b, c, d, e, f);
-		if (ez.getSolverTimoutStatus())
+		ez->setSolverTimeout(timeout);
+		bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f);
+		if (ez->getSolverTimoutStatus())
 			gotTimeout = true;
 		return success;
 	}
@@ -478,7 +479,7 @@ struct SatHelper
 					maybe_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i));
 
 			backupValues.swap(modelValues);
-			if (!solve(ez.expression(ezSAT::OpAnd, must_undef), ez.expression(ezSAT::OpOr, maybe_undef)))
+			if (!solve(ez->expression(ezSAT::OpAnd, must_undef), ez->expression(ezSAT::OpOr, maybe_undef)))
 				break;
 		}
 
@@ -832,12 +833,12 @@ struct SatHelper
 				int bit = modelExpressions.at(i), bit_undef = modelExpressions.at(modelExpressions.size()/2 + i);
 				bool val = modelValues.at(i), val_undef = modelValues.at(modelExpressions.size()/2 + i);
 				if (!max_undef || !val_undef)
-					clause.push_back(val_undef ? ez.NOT(bit_undef) : val ? ez.NOT(bit) : bit);
+					clause.push_back(val_undef ? ez->NOT(bit_undef) : val ? ez->NOT(bit) : bit);
 			}
 		} else
 			for (size_t i = 0; i < modelExpressions.size(); i++)
-				clause.push_back(modelValues.at(i) ? ez.NOT(modelExpressions.at(i)) : modelExpressions.at(i));
-		ez.assume(ez.expression(ezSAT::OpOr, clause));
+				clause.push_back(modelValues.at(i) ? ez->NOT(modelExpressions.at(i)) : modelExpressions.at(i));
+		ez->assume(ez->expression(ezSAT::OpOr, clause));
 	}
 };
 
@@ -1319,11 +1320,11 @@ struct SatPass : public Pass {
 			inductstep.ignore_unknown_cells = ignore_unknown_cells;
 
 			inductstep.setup(1);
-			inductstep.ez.assume(inductstep.setup_proof(1));
+			inductstep.ez->assume(inductstep.setup_proof(1));
 
 			if (tempinduct_def) {
 				std::vector<int> undef_state = inductstep.satgen.importUndefSigSpec(inductstep.satgen.initial_state.export_all(), 1);
-				inductstep.ez.assume(inductstep.ez.NOT(inductstep.ez.expression(ezSAT::OpOr, undef_state)));
+				inductstep.ez->assume(inductstep.ez->NOT(inductstep.ez->expression(ezSAT::OpOr, undef_state)));
 			}
 
 			for (int inductlen = 1; inductlen <= maxsteps || maxsteps == 0; inductlen++)
@@ -1340,9 +1341,9 @@ struct SatPass : public Pass {
 					basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
 
 				log("\n[base case] Solving problem with %d variables and %d clauses..\n",
-						basecase.ez.numCnfVariables(), basecase.ez.numCnfClauses());
+						basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses());
 
-				if (basecase.solve(basecase.ez.NOT(property))) {
+				if (basecase.solve(basecase.ez->NOT(property))) {
 					log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
 					print_proof_failed();
 					basecase.print_model();
@@ -1357,7 +1358,7 @@ struct SatPass : public Pass {
 					goto timeout;
 
 				log("Base case for induction length %d proven.\n", inductlen);
-				basecase.ez.assume(property);
+				basecase.ez->assume(property);
 
 				// phase 2: proving induction step
 
@@ -1371,8 +1372,8 @@ struct SatPass : public Pass {
 				if (inductlen < initsteps)
 				{
 					log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n",
-							inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
-					inductstep.ez.assume(property);
+							inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
+					inductstep.ez->assume(property);
 				}
 				else
 				{
@@ -1385,14 +1386,14 @@ struct SatPass : public Pass {
 						log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
 						cnf_file_name.clear();
 
-						inductstep.ez.printDIMACS(f, false);
+						inductstep.ez->printDIMACS(f, false);
 						fclose(f);
 					}
 
 					log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
-							inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
+							inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
 
-					if (!inductstep.solve(inductstep.ez.NOT(property))) {
+					if (!inductstep.solve(inductstep.ez->NOT(property))) {
 						if (inductstep.gotTimeout)
 							goto timeout;
 						log("Induction step proven: SUCCESS!\n");
@@ -1401,7 +1402,7 @@ struct SatPass : public Pass {
 					}
 
 					log("Induction step failed. Incrementing induction length.\n");
-					inductstep.ez.assume(property);
+					inductstep.ez->assume(property);
 					inductstep.print_model();
 				}
 			}
@@ -1457,7 +1458,7 @@ struct SatPass : public Pass {
 			if (seq_len == 0) {
 				sathelper.setup();
 				if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
-					sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
+					sathelper.ez->assume(sathelper.ez->NOT(sathelper.setup_proof()));
 			} else {
 				std::vector<int> prove_bits;
 				for (int timestep = 1; timestep <= seq_len; timestep++) {
@@ -1467,7 +1468,7 @@ struct SatPass : public Pass {
 							prove_bits.push_back(sathelper.setup_proof(timestep));
 				}
 				if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
-					sathelper.ez.assume(sathelper.ez.NOT(sathelper.ez.expression(ezSAT::OpAnd, prove_bits)));
+					sathelper.ez->assume(sathelper.ez->NOT(sathelper.ez->expression(ezSAT::OpAnd, prove_bits)));
 				sathelper.setup_init();
 			}
 			sathelper.generate_model();
@@ -1481,7 +1482,7 @@ struct SatPass : public Pass {
 				log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
 				cnf_file_name.clear();
 
-				sathelper.ez.printDIMACS(f, false);
+				sathelper.ez->printDIMACS(f, false);
 				fclose(f);
 			}
 
@@ -1489,7 +1490,7 @@ struct SatPass : public Pass {
 
 		rerun_solver:
 			log("\nSolving problem with %d variables and %d clauses..\n",
-					sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses());
+					sathelper.ez->numCnfVariables(), sathelper.ez->numCnfClauses());
 
 			if (sathelper.solve())
 			{