diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 1f4b8855f..a820405ac 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -104,6 +104,8 @@ bool ezMiniSAT::solver(const std::vector<int> &modelExpressions, std::vector<boo
 	preSolverCallback();
 
 	solverTimeoutStatus = false;
+	solverPropLimitStatus = false;
+	solverProps = 0;
 
 	if (0) {
 contradiction:
@@ -201,7 +203,21 @@ contradiction:
 	}
 #endif
 
-	bool foundSolution = minisatSolver->solve(assumps);
+	uint64_t solverPropsBefore = minisatSolver->propagations;
+	bool foundSolution;
+
+	if (solverPropLimit > 0) {
+		minisatSolver->setPropBudget(solverPropLimit);
+		Minisat::lbool res = minisatSolver->solveLimited(assumps);
+		minisatSolver->budgetOff();
+		if (Minisat::toInt(res) == 2) // l_Undef: propagation budget exhausted
+			solverPropLimitStatus = true;
+		foundSolution = (Minisat::toInt(res) == 0); // l_True
+	} else {
+		foundSolution = minisatSolver->solve(assumps);
+	}
+
+	solverProps = minisatSolver->propagations - solverPropsBefore;
 
 #if defined(HAS_ALARM)
 	if (solverTimeout > 0) {
@@ -210,6 +226,7 @@ contradiction:
 		alarm(0);
 		sigaction(SIGALRM, &old_sig_action, NULL);
 		alarm(old_alarm_timeout);
+		minisatSolver->clearInterrupt();
 	}
 #endif
 
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 8e3114705..e5cdf84c1 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -55,6 +55,9 @@ ezSAT::ezSAT()
 
 	solverTimeout = 0;
 	solverTimeoutStatus = false;
+	solverPropLimit = 0;
+	solverPropLimitStatus = false;
+	solverProps = 0;
 
 	literal("CONST_TRUE");
 	literal("CONST_FALSE");
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 445c8edba..77496b89f 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -79,6 +79,9 @@ protected:
 public:
 	int solverTimeout;
 	bool solverTimeoutStatus;
+	int64_t solverPropLimit;
+	bool solverPropLimitStatus;
+	int64_t solverProps;
 
 	ezSAT();
 	virtual ~ezSAT();
@@ -157,6 +160,19 @@ public:
 		return solverTimeoutStatus;
 	}
 
+	void setSolverPropLimit(int64_t newPropLimit) {
+		solverPropLimit = newPropLimit;
+	}
+
+	bool getSolverPropLimitStatus() {
+		return solverPropLimitStatus;
+	}
+
+	// propagations spent by the most recent solve() call
+	int64_t getSolverProps() {
+		return solverProps;
+	}
+
 	// manage CNF (usually only accessed by SAT solvers)
 
 	virtual void clear();